---

Step * 2 1 1 1 1 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
17. sab : a ≠ b
18. scd : c ≠ d
19. <a, b, sab> ∈ Line
20. <c, d, scd> ∈ Line
21. a ≠ b ∧ c ≠ d
⊢ ∃a@0,b:{c:Point| c I <a, b, sab>} . (a@0 leftof cd ∧ b leftof dc)
BY
{ (InstConcl [⌜a⌝;⌜b⌝]⋅ THEN Auto THEN Try ((MemTypeCD THEN Auto)) THEN Try ((SubsumeC ⌜Line⌝⋅ THEN Auto))) }

1
.....set predicate..... 
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
19. <a, b, sab> ∈ Line
20. <c, d, scd> ∈ Line
21. a ≠ b
22. c ≠ d
⊢ a I <a, b, sab>

2
.....set predicate..... 
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
19. <a, b, sab> ∈ Line
20. <c, d, scd> ∈ Line
21. a ≠ b
22. c ≠ d
⊢ b I <a, b, sab>

---

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
17.  sab  :  a  \mneq{}  b
18.  scd  :  c  \mneq{}  d
19.  <a,  b,  sab>  \mmember{}  Line
20.  <c,  d,  scd>  \mmember{}  Line
21.  a  \mneq{}  b  \mwedge{}  c  \mneq{}  d
\mvdash{}  \mexists{}a@0,b:\{c:Point|  c  I  <a,  b,  sab>\}  .  (a@0  leftof  cd  \mwedge{}  b  leftof  dc)


By

---

Latex:
(InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((MemTypeCD  THEN  Auto))
  THEN  Try  ((SubsumeC  \mkleeneopen{}Line\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index