---

Step * of Lemma geo-parallel-strict

∀e:EuclideanPlane. ∀a,b:Point.  (geo-parallel(e;a;b;a;b) ⇒ False)
BY
{ ((((Auto THEN D -1) THEN InstHyp [⌜a⌝] (5)⋅ THEN Auto) THEN (Assert a ≡ a BY Auto) THEN (Assert a ≠ a BY Auto))
   THEN Auto
   ) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b:Point.    (geo-parallel(e;a;b;a;b)  {}\mRightarrow{}  False)


By

---

Latex:
((((Auto  THEN  D  -1)  THEN  InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (5)\mcdot{}  THEN  Auto)
    THEN  (Assert  a  \mequiv{}  a  BY
                            Auto)
    THEN  (Assert  a  \mneq{}  a  BY
                            Auto))
  THEN  Auto
  )

---

Home Index