---

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


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. ¬((¬B_C_D) ∧ (¬B_D_C))
10. ¬(B = C ∈ Point)
⊢ Colinear(B;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. ¬((¬B_C_D) ∧ (¬B_D_C))
10. ¬(B = C ∈ Point)
11. (¬(D = B ∈ Point)) ∧ (¬(D = C ∈ Point)) ∧ (¬D-B-C) ∧ (¬B-D-C) ∧ (¬B-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{}B\_C\_D)  \mwedge{}  (\mneg{}B\_D\_C))
10.  \mneg{}(B  =  C)
\mvdash{}  Colinear(B;C;D)


By

---

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

---

Home Index