---

Step * 1 1 of Lemma geo-intersect-iff


1. e : EuclideanPlane
2. l : Line
3. p : Line
4. a : {a:Point| a I p} 
5. b : {c:Point| c I p} 
6. a leftof fst(l)fst(snd(l))
7. b leftof fst(snd(l))fst(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)
BY
{ (RepeatFor 2 (D -5)
   THEN RepeatFor 2 (D -8)
   THEN All Reduce
   THEN ExRepD
   THEN (GenConclTerm ⌜geo-SS(e;x1;y1;a;b)⌝⋅ THENA Auto)
   THEN Thin (-1)) }

1
1. e : EuclideanPlane
2. x1 : Point
3. y1 : Point
4. l2 : x1 ≠ y1
5. x : Point
6. y : Point
7. p2 : x ≠ y
8. a : {a:Point| a I <x, y, p2>} 
9. b : {c:Point| c I <x, y, p2>} 
10. a leftof x1y1
11. b leftof y1x1
12. v : {x:Point| Colinear(x1;y1;x) ∧ a_x_b} 
⊢ ∃a,b,c,d,v:Point. (a-v-b ∧ c-v-d ∧ a I <x, y, p2> ∧ b I <x, y, p2> ∧ c I <x1, y1, l2> ∧ d I <x1, y1, l2> ∧ a leftof cd\000C ∧ b leftof dc)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  l  :  Line
3.  p  :  Line
4.  a  :  \{a:Point|  a  I  p\} 
5.  b  :  \{c:Point|  c  I  p\} 
6.  a  leftof  fst(l)fst(snd(l))
7.  b  leftof  fst(snd(l))fst(l)
\mvdash{}  \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)


By

---

Latex:
(RepeatFor  2  (D  -5)
  THEN  RepeatFor  2  (D  -8)
  THEN  All  Reduce
  THEN  ExRepD
  THEN  (GenConclTerm  \mkleeneopen{}geo-SS(e;x1;y1;a;b)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index