---

Step * 1 of Lemma geo-intersect-iff


1. e : EuclideanPlane
2. P : LINE
3. L : LINE
4. 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)
BY
{ (D -1
   THEN ExRepD
   THEN (Eliminate ⌜P⌝⋅ THENA Auto)
   THEN (Eliminate ⌜L⌝⋅ THENA Auto)
   THEN ThinVar `P'
   THEN ThinVar `L'
   THEN RenameTo `p' `m'
   THEN SwapVars `l' `p') }

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

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  P  :  LINE
3.  L  :  LINE
4.  P  \mbackslash{}/  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:
(D  -1
  THEN  ExRepD
  THEN  (Eliminate  \mkleeneopen{}P\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Eliminate  \mkleeneopen{}L\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `P'
  THEN  ThinVar  `L'
  THEN  RenameTo  `p'  `m'
  THEN  SwapVars  `l'  `p')

---

Home Index