Mizar/本体部/結果

証明終了は次のいずれかになる。

thus ～;
hence ～;
よって、それ故に、故に

hence は then + thus ということです。

---

式より矛盾する

式;
thus contradiction;

---

式より矛盾しない

式;
thus not contradiction;

---

---

ラベル1,ラベル2の式によって示せた

ラベル1:式1;
...
ラベル2:式2;
hence thesis by ラベル1;

---

ラベル1,ラベル2の式によって結果 が示せた

ラベル1:式1;
ラベル2:式2;
...
thus 結果 by ラベル1,ラベル2;

ラベル1:式1;
...
ラベル2:式2;
hence 結果 by ラベル1;