---

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


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
BY
{ (ExRepD
   THEN D 9
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN (RWO "eu-between-eq-def" (-1) THENA Auto)
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:

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.  \mneg{}(A  =  B)
9.  \mneg{}((\mneg{}B\_C\_D)  \mwedge{}  (\mneg{}B\_D\_C))
10.  \mneg{}(B  =  C)
11.  (\mneg{}(D  =  B))  \mwedge{}  (\mneg{}(D  =  C))  \mwedge{}  (\mneg{}D-B-C)  \mwedge{}  (\mneg{}B-D-C)  \mwedge{}  (\mneg{}B-C-D)@i
\mvdash{}  False


By

---

Latex:
(ExRepD
  THEN  D  9
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  (RWO  "eu-between-eq-def"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index