---

Step * 2 1 of Lemma geo-intersect-iff


1. e : EuclideanPlane
2. P : LINE
3. L : LINE
4. a : Point
5. b : Point
6. c : Point
7. d : Point
8. v : Point
9. a-v-b
10. c-v-d
11. a I P
12. b I P
13. c I L
14. d I L
15. a leftof cd
16. b leftof dc
⊢ P \/ L
BY
{ (((Assert a ≠ b BY Auto) THEN RenameVar `sab' (-1)) THEN (Assert c ≠ d BY Auto) THEN RenameVar `scd' (-1)) }

1
1. e : EuclideanPlane
2. P : LINE
3. L : LINE
4. a : Point
5. b : Point
6. c : Point
7. d : Point
8. v : Point
9. a-v-b
10. c-v-d
11. a I P
12. b I P
13. c I L
14. d I L
15. a leftof cd
16. b leftof dc
17. sab : a ≠ b
18. scd : c ≠ d
⊢ P \/ L

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  P  :  LINE
3.  L  :  LINE
4.  a  :  Point
5.  b  :  Point
6.  c  :  Point
7.  d  :  Point
8.  v  :  Point
9.  a-v-b
10.  c-v-d
11.  a  I  P
12.  b  I  P
13.  c  I  L
14.  d  I  L
15.  a  leftof  cd
16.  b  leftof  dc
\mvdash{}  P  \mbackslash{}/  L


By

---

Latex:
(((Assert  a  \mneq{}  b  BY  Auto)  THEN  RenameVar  `sab'  (-1))
  THEN  (Assert  c  \mneq{}  d  BY
                          Auto)
  THEN  RenameVar  `scd'  (-1))

---

Home Index