---

Step * 1 1 1 of Lemma geo-intersect-irreflexive


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. v : Point
7. a-v-b
8. c-v-d
9. a leftof cd
10. b leftof dc
11. c leftof ba
12. d leftof ab
13. sab : a ≠ b
14. scd : c ≠ d
15. <a, b, sab> = <c, d, scd> ∈ LINE
⊢ False
BY
{ (((EqTypeHD  (-1) THENA Auto) THEN FLemma `geo-line-eq-to-col` [-1] THEN Reduce -1) THENA Auto) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. v : Point
7. a-v-b
8. c-v-d
9. a leftof cd
10. b leftof dc
11. c leftof ba
12. d leftof ab
13. sab : a ≠ b
14. scd : c ≠ d
15. <a, b, sab> = <c, d, scd> ∈ pertype(λl,m. ((l ∈ Line) ∧ (m ∈ Line) ∧ l ≡ m))
16. <a, b, sab> ∈ Line
17. <c, d, scd> ∈ Line
18. <a, b, sab> ≡ <c, d, scd>
19. Colinear(a;b;c) ∧ Colinear(a;b;d)
⊢ False

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  v  :  Point
7.  a-v-b
8.  c-v-d
9.  a  leftof  cd
10.  b  leftof  dc
11.  c  leftof  ba
12.  d  leftof  ab
13.  sab  :  a  \mneq{}  b
14.  scd  :  c  \mneq{}  d
15.  <a,  b,  sab>  =  <c,  d,  scd>
\mvdash{}  False


By

---

Latex:
(((EqTypeHD    (-1)  THENA  Auto)  THEN  FLemma  `geo-line-eq-to-col`  [-1]  THEN  Reduce  -1)  THENA  Auto)

---

Home Index