---

Step * of Lemma eu-between-implies-colinear

∀e:EuclideanStructure. ∀[a,b,c:Point].  (Colinear(a;b;c)) supposing (a-b-c and (¬(a = b ∈ Point)))
BY
{ (InstLemma `eu-between-eq-implies-colinear` [] THEN RepeatFor 6 (ParallelLast') THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanStructure.  \mforall{}[a,b,c:Point].    (Colinear(a;b;c))  supposing  (a-b-c  and  (\mneg{}(a  =  b)))


By

---

Latex:
(InstLemma  `eu-between-eq-implies-colinear`  []  THEN  RepeatFor  6  (ParallelLast')  THEN  EAuto  1)

---

Home Index