---

Step * 1 1 of Lemma geo-intersect-irreflexive


1. g : EuclideanPlane
2. m : LINE
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. v : Point
8. a-v-b
9. c-v-d
10. a I m
11. b I m
12. c I m
13. d I m
14. a leftof cd
15. b leftof dc
16. c leftof ba
17. d leftof ab
18. sab : a ≠ b
19. <a, b, sab> = m ∈ LINE
20. scd : c ≠ d
21. <c, d, scd> = m ∈ LINE
⊢ False
BY
{ ((Assert <a, b, sab> = <c, d, scd> ∈ LINE BY Eq) THEN ThinVar `m') }

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> ∈ LINE
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  <a,  b,  sab>  =  <c,  d,  scd>  BY  Eq)  THEN  ThinVar  `m')

---

Home Index