---

Step * of Lemma geo-intersect-iff3

∀e:EuclideanPlane. ∀p,l:LINE.
  (p \/ l
  ⇐⇒ ∃a,b,c,d,v:Point
       ∃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
{ (InstLemma `geo-intersect-iff2` []
   THEN RepeatFor 3 (ParallelLast')
   THEN D -1
   THEN (D 0 THENL [Thin (-1); Thin (-2)⋅])
   THEN RepeatFor 6 (ParallelLast)
   THEN ExRepD) }

1
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)

2
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)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}p,l:LINE.
    (p  \mbackslash{}/  l
    \mLeftarrow{}{}\mRightarrow{}  \mexists{}a,b,c,d,v:Point
              \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:
(InstLemma  `geo-intersect-iff2`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  D  -1
  THEN  (D  0  THENL  [Thin  (-1);  Thin  (-2)\mcdot{}])
  THEN  RepeatFor  6  (ParallelLast)
  THEN  ExRepD)

---

Home Index