---

Step * 1 of Lemma eu-colinear-between


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)
BY
{ (ProperProlong ⌜B⌝ ⌜A⌝ `t' ⌜O⌝ ⌜X⌝⋅ 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)
10. t : Point
11. B-A-t ∧ At=OX
⊢ Colinear(A;C;D)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  D  :  Point
6.  A\_D\_B
7.  A\_C\_B
8.  \mneg{}(A  =  B)
9.  \mneg{}(A  =  C)
\mvdash{}  Colinear(A;C;D)


By

---

Latex:
(ProperProlong  \mkleeneopen{}B\mkleeneclose{}  \mkleeneopen{}A\mkleeneclose{}  `t'  \mkleeneopen{}O\mkleeneclose{}  \mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index