---

Step * 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
⊢ False
BY
{ ((((Assert a ≠ b BY Auto) THEN RenameVar `sab' (-1))
    THEN (Assert <a, b, sab> = m ∈ LINE BY
                (BLemma `geo-line-eq-geoline` THEN Auto))
    )
   THEN ((Assert c ≠ d BY Auto) THEN RenameVar `scd' (-1))
   THEN (Assert <c, d, scd> = m ∈ LINE BY
               (BLemma `geo-line-eq-geoline` THEN Auto))) }

1
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

---

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
\mvdash{}  False


By

---

Latex:
((((Assert  a  \mneq{}  b  BY  Auto)  THEN  RenameVar  `sab'  (-1))
    THEN  (Assert  <a,  b,  sab>  =  m  BY
                            (BLemma  `geo-line-eq-geoline`  THEN  Auto))
    )
  THEN  ((Assert  c  \mneq{}  d  BY  Auto)  THEN  RenameVar  `scd'  (-1))
  THEN  (Assert  <c,  d,  scd>  =  m  BY
                          (BLemma  `geo-line-eq-geoline`  THEN  Auto)))

---

Home Index