---

Step * of Lemma geo-intersect-points-iff

∀e:EuclideanPlane. ∀a,b,c,d:Point.
  (ab \/ cd
  ⇐⇒ a ≠ b
      ∧ c ≠ d
      ∧ (∃a1,b1,c1,d1,v:Point
          (a1-v-b1
          ∧ c1-v-d1
          ∧ Colinear(a1;a;b)
          ∧ Colinear(b1;a;b)
          ∧ Colinear(c1;c;d)
          ∧ Colinear(d1;c;d)
          ∧ a1 leftof c1d1
          ∧ b1 leftof d1c1)))
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab \/ cd
⊢ c ≠ d

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab \/ cd
⊢ ∃a1,b1,c1,d1,v:Point
   (a1-v-b1
   ∧ c1-v-d1
   ∧ Colinear(a1;a;b)
   ∧ Colinear(b1;a;b)
   ∧ Colinear(c1;c;d)
   ∧ Colinear(d1;c;d)
   ∧ a1 leftof c1d1
   ∧ b1 leftof d1c1)

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b
7. c ≠ d
8. ∃a1,b1,c1,d1,v:Point
    (a1-v-b1
    ∧ c1-v-d1
    ∧ Colinear(a1;a;b)
    ∧ Colinear(b1;a;b)
    ∧ Colinear(c1;c;d)
    ∧ Colinear(d1;c;d)
    ∧ a1 leftof c1d1
    ∧ b1 leftof d1c1)
⊢ ab \/ cd

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.
    (ab  \mbackslash{}/  cd
    \mLeftarrow{}{}\mRightarrow{}  a  \mneq{}  b
            \mwedge{}  c  \mneq{}  d
            \mwedge{}  (\mexists{}a1,b1,c1,d1,v:Point
                    (a1-v-b1
                    \mwedge{}  c1-v-d1
                    \mwedge{}  Colinear(a1;a;b)
                    \mwedge{}  Colinear(b1;a;b)
                    \mwedge{}  Colinear(c1;c;d)
                    \mwedge{}  Colinear(d1;c;d)
                    \mwedge{}  a1  leftof  c1d1
                    \mwedge{}  b1  leftof  d1c1)))


By

---

Latex:
Auto

---

Home Index