---

Step * of Lemma eu-colinear-between

∀e:EuclideanPlane
  ∀[A,B,C,D:Point].  (Colinear(A;C;D)) supposing ((¬(A = C ∈ Point)) and (¬(A = B ∈ Point)) and A_C_B and A_D_B)
BY
{ (Auto THEN (Unhide THENA Auto)) }

1
1. e : EuclideanPlane
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. A_D_B
7. A_C_B
8. ¬(A = B ∈ Point)
9. ¬(A = C ∈ Point)
⊢ Colinear(A;C;D)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane
    \mforall{}[A,B,C,D:Point].    (Colinear(A;C;D))  supposing  ((\mneg{}(A  =  C))  and  (\mneg{}(A  =  B))  and  A\_C\_B  and  A\_D\_B)


By

---

Latex:
(Auto  THEN  (Unhide  THENA  Auto))

---

Home Index