---

Step * of Lemma geo-intersect-points-iff2

No Annotations
∀e:EuclideanPlane. ∀p1,p2,l1,l2:Point.
  (p1p2 \/ l1l2
  ⇐⇒ p1 # p2
      ∧ l1 # l2
      ∧ (∃a,b,c,d,v:Point
          (a-v-b
          ∧ c-v-d
          ∧ Colinear(a;p1;p2)
          ∧ Colinear(b;p1;p2)
          ∧ Colinear(c;l1;l2)
          ∧ Colinear(d;l1;l2)
          ∧ a leftof cd
          ∧ b leftof dc
          ∧ c leftof ba
          ∧ d leftof ab)))
BY
{ (Intros
   THEN (RWO "geo-intersect-points-iff" 0 THENA Auto)
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN RepeatFor 5 (ParallelLast)
   THEN Auto) }

1
1. e : EuclideanPlane
2. p1 : Point
3. p2 : Point
4. l1 : Point
5. l2 : Point
6. p1 # p2
7. l1 # l2
8. a1 : Point
9. b1 : Point
10. c1 : Point
11. ∃d1,v:Point
     (a1-v-b1
     ∧ c1-v-d1
     ∧ Colinear(a1;p1;p2)
     ∧ Colinear(b1;p1;p2)
     ∧ Colinear(c1;l1;l2)
     ∧ Colinear(d1;l1;l2)
     ∧ a1 leftof c1d1
     ∧ b1 leftof d1c1)
⊢ ∃d,v:Point
   (a1-v-b1
   ∧ c1-v-d
   ∧ Colinear(a1;p1;p2)
   ∧ Colinear(b1;p1;p2)
   ∧ Colinear(c1;l1;l2)
   ∧ Colinear(d;l1;l2)
   ∧ a1 leftof c1d
   ∧ b1 leftof dc1
   ∧ c1 leftof b1a1
   ∧ d leftof a1b1)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}p1,p2,l1,l2:Point.
    (p1p2  \mbackslash{}/  l1l2
    \mLeftarrow{}{}\mRightarrow{}  p1  \#  p2
            \mwedge{}  l1  \#  l2
            \mwedge{}  (\mexists{}a,b,c,d,v:Point
                    (a-v-b
                    \mwedge{}  c-v-d
                    \mwedge{}  Colinear(a;p1;p2)
                    \mwedge{}  Colinear(b;p1;p2)
                    \mwedge{}  Colinear(c;l1;l2)
                    \mwedge{}  Colinear(d;l1;l2)
                    \mwedge{}  a  leftof  cd
                    \mwedge{}  b  leftof  dc
                    \mwedge{}  c  leftof  ba
                    \mwedge{}  d  leftof  ab)))


By

---

Latex:
(Intros
  THEN  (RWO  "geo-intersect-points-iff"  0  THENA  Auto)
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  RepeatFor  5  (ParallelLast)
  THEN  Auto)

---

Home Index