---

Step * 1 of Lemma geo-intersect-iff3


1. e : EuclideanPlane
2. p : LINE
3. l : LINE
4. p \/ l
5. a : Point
6. b : Point
7. c : Point
8. d : Point
9. v : Point
10. a-v-b
11. c-v-d
12. a I p
13. b I p
14. c I l
15. d I l
16. a leftof cd
17. b leftof dc
18. c leftof ba
19. d leftof ab
⊢ ∃sab:a ≠ b
   ∃scd:c ≠ d
    ((p = <a, b, sab> ∈ LINE)
    ∧ (l = <c, d, scd> ∈ LINE)
    ∧ a-v-b
    ∧ c-v-d
    ∧ a leftof cd
    ∧ b leftof dc
    ∧ c leftof ba
    ∧ d leftof ab)
BY
{ (((Assert a ≠ b BY
           Auto)
    THEN RenameVar `sab' (-1)
    THEN (D 0 With ⌜sab⌝  THENA (Auto THEN SubsumeC ⌜Line⌝⋅ THEN Auto)))
   THEN (Assert c ≠ d BY
               Auto)
   THEN RenameVar `scd' (-1)
   THEN (D 0 With ⌜scd⌝  THENA (Auto THEN SubsumeC ⌜Line⌝⋅ THEN Auto))
   THEN Auto
   THEN Symmetry
   THEN BLemma `geo-line-eq-geoline`
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  p  :  LINE
3.  l  :  LINE
4.  p  \mbackslash{}/  l
5.  a  :  Point
6.  b  :  Point
7.  c  :  Point
8.  d  :  Point
9.  v  :  Point
10.  a-v-b
11.  c-v-d
12.  a  I  p
13.  b  I  p
14.  c  I  l
15.  d  I  l
16.  a  leftof  cd
17.  b  leftof  dc
18.  c  leftof  ba
19.  d  leftof  ab
\mvdash{}  \mexists{}sab:a  \mneq{}  b
      \mexists{}scd:c  \mneq{}  d
        ((p  =  <a,  b,  sab>)
        \mwedge{}  (l  =  <c,  d,  scd>)
        \mwedge{}  a-v-b
        \mwedge{}  c-v-d
        \mwedge{}  a  leftof  cd
        \mwedge{}  b  leftof  dc
        \mwedge{}  c  leftof  ba
        \mwedge{}  d  leftof  ab)


By

---

Latex:
(((Assert  a  \mneq{}  b  BY
                  Auto)
    THEN  RenameVar  `sab'  (-1)
    THEN  (D  0  With  \mkleeneopen{}sab\mkleeneclose{}    THENA  (Auto  THEN  SubsumeC  \mkleeneopen{}Line\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  (Assert  c  \mneq{}  d  BY
                          Auto)
  THEN  RenameVar  `scd'  (-1)
  THEN  (D  0  With  \mkleeneopen{}scd\mkleeneclose{}    THENA  (Auto  THEN  SubsumeC  \mkleeneopen{}Line\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Auto
  THEN  Symmetry
  THEN  BLemma  `geo-line-eq-geoline`
  THEN  Reduce  0
  THEN  Auto)

---

Home Index