---

Step * of Lemma eu-between-eq-exchange3

∀e:EuclideanPlane. ∀[a,b,c,d:Point].  (b_c_d) supposing (a_c_d and a_b_c)
BY
{ (Auto THEN (Unhide THENA Auto) THEN EuContradiction) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[a,b,c,d:Point].    (b\_c\_d)  supposing  (a\_c\_d  and  a\_b\_c)


By

---

Latex:
(Auto  THEN  (Unhide  THENA  Auto)  THEN  EuContradiction)

---

Home Index