---

Step * of Lemma geo-intersect-iff2

∀e:EuclideanPlane. ∀p,l:LINE.
  (p \/ l
  ⇐⇒ ∃a,b,c,d,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
{ (Intros
   THEN (RWO "geo-intersect-iff" 0 THENA Auto)
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN RepeatFor 5 (ParallelLast)
   THEN 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. 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. a-v-b
18. c-v-d
19. a I p
20. b I p
21. c I l
22. d I l
23. a leftof cd
24. b leftof dc
⊢ c leftof ba

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. 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. a-v-b
18. c-v-d
19. a I p
20. b I p
21. c I l
22. d I l
23. a leftof cd
24. b leftof dc
25. 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
              (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:
(Intros
  THEN  (RWO  "geo-intersect-iff"  0  THENA  Auto)
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  RepeatFor  5  (ParallelLast)
  THEN  Auto)

---

Home Index