---

Step * 1 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> ∈ 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
BY
{ D -1 }

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)
20. 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>
16.  <a,  b,  sab>  \mmember{}  Line
17.  <c,  d,  scd>  \mmember{}  Line
18.  <a,  b,  sab>  \mequiv{}  <c,  d,  scd>
19.  Colinear(a;b;c)  \mwedge{}  Colinear(a;b;d)
\mvdash{}  False


By

---

Latex:
D  -1

---

Home Index