---

Step * 2 of Lemma geo-intersect-iff3


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. sab : a ≠ b
10. scd : c ≠ d
11. p = <a, b, sab> ∈ LINE
12. l = <c, d, scd> ∈ LINE
13. a-v-b
14. c-v-d
15. a leftof cd
16. b leftof dc
17. c leftof ba
18. d leftof ab
⊢ ∃v:Point. (a-v-b ∧ c-v-d ∧ a I p ∧ b I p ∧ c I l ∧ d I l ∧ a leftof cd ∧ b leftof dc ∧ c leftof ba ∧ d leftof ab)
BY
{ (D 0 With ⌜v⌝  THENA Auto) }

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. sab : a ≠ b
10. scd : c ≠ d
11. p = <a, b, sab> ∈ LINE
12. l = <c, d, scd> ∈ LINE
13. a-v-b
14. c-v-d
15. a leftof cd
16. b leftof dc
17. c leftof ba
18. d leftof ab
⊢ a-v-b ∧ c-v-d ∧ a I p ∧ b I p ∧ c I l ∧ d I l ∧ a leftof cd ∧ b leftof dc ∧ c leftof ba ∧ d leftof ab

---

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.  sab  :  a  \mneq{}  b
10.  scd  :  c  \mneq{}  d
11.  p  =  <a,  b,  sab>
12.  l  =  <c,  d,  scd>
13.  a-v-b
14.  c-v-d
15.  a  leftof  cd
16.  b  leftof  dc
17.  c  leftof  ba
18.  d  leftof  ab
\mvdash{}  \mexists{}v:Point
      (a-v-b
      \mwedge{}  c-v-d
      \mwedge{}  a  I  p
      \mwedge{}  b  I  p
      \mwedge{}  c  I  l
      \mwedge{}  d  I  l
      \mwedge{}  a  leftof  cd
      \mwedge{}  b  leftof  dc
      \mwedge{}  c  leftof  ba
      \mwedge{}  d  leftof  ab)


By

---

Latex:
(D  0  With  \mkleeneopen{}v\mkleeneclose{}    THENA  Auto)

---

Home Index