---

Step * 1 of Lemma eu-colinear-same-side2


1. e : EuclideanPlane@i'
2. [A] : Point
3. [B] : Point
4. [C] : Point
5. [D] : Point
6. [%1] : A_B_D
7. [%] : A_B_C
8. ¬(A = B ∈ Point)
9. ¬((¬A_C_D) ∧ (¬A_D_C))
10. ¬(A = C ∈ Point)
⊢ Colinear(A;C;D)
BY
{ (((RWO "eu-colinear-def" 0 THENM RepeatFor 2 (D 0)) THENA Auto) THEN Unhide THEN Try (Trivial)) }

1
1. e : EuclideanPlane@i'
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. A_B_D
7. A_B_C
8. ¬(A = B ∈ Point)
9. ¬((¬A_C_D) ∧ (¬A_D_C))
10. ¬(A = C ∈ Point)
11. (¬(D = A ∈ Point)) ∧ (¬(D = C ∈ Point)) ∧ (¬D-A-C) ∧ (¬A-D-C) ∧ (¬A-C-D)@i
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  [A]  :  Point
3.  [B]  :  Point
4.  [C]  :  Point
5.  [D]  :  Point
6.  [\%1]  :  A\_B\_D
7.  [\%]  :  A\_B\_C
8.  \mneg{}(A  =  B)
9.  \mneg{}((\mneg{}A\_C\_D)  \mwedge{}  (\mneg{}A\_D\_C))
10.  \mneg{}(A  =  C)
\mvdash{}  Colinear(A;C;D)


By

---

Latex:
(((RWO  "eu-colinear-def"  0  THENM  RepeatFor  2  (D  0))  THENA  Auto)  THEN  Unhide  THEN  Try  (Trivial))

---

Home Index