---

Step * 3 of Lemma geo-intersect-points-iff


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
BY
{ ((ExRepD THEN D 0 THEN Try (Auto))
   THEN (Assert a1 # cd ∧ b1 # cd BY
               ((InstLemma `colinear-lsep-general` [⌜e⌝;⌜c1⌝;⌜d1⌝;⌜c⌝;⌜d⌝]⋅ THENA Auto)
                THEN (InstHyp [⌜a1⌝] (-1)⋅ THEN Auto)
                THEN InstHyp [⌜b1⌝] (-2)⋅
                THEN Auto))
   ) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b
7. c ≠ d
8. a1 : Point
9. b1 : Point
10. c1 : Point
11. d1 : Point
12. v : Point
13. a1-v-b1
14. c1-v-d1
15. Colinear(a1;a;b)
16. Colinear(b1;a;b)
17. Colinear(c1;c;d)
18. Colinear(d1;c;d)
19. a1 leftof c1d1
20. b1 leftof d1c1
21. a1 # cd ∧ b1 # cd
⊢ ∃x,y:{z:Point| Colinear(z;a;b)} . (x leftof cd ∧ y leftof dc)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  a  \mneq{}  b
7.  c  \mneq{}  d
8.  \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)
\mvdash{}  ab  \mbackslash{}/  cd


By

---

Latex:
((ExRepD  THEN  D  0  THEN  Try  (Auto))
  THEN  (Assert  a1  \#  cd  \mwedge{}  b1  \#  cd  BY
                          ((InstLemma  `colinear-lsep-general`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (InstHyp  [\mkleeneopen{}a1\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
                            THEN  InstHyp  [\mkleeneopen{}b1\mkleeneclose{}]  (-2)\mcdot{}
                            THEN  Auto))
  )

---

Home Index