---

Step * 1 1 1 of Lemma Euclid-parallel-points-exists


1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. p : Point
5. z : Point
6. u : Point
7. q : Point
8. Colinear(u;z;p)
9. ab  ⊥u uz
10. z # ab
11. z # p
12. zp  ⊥p qp
13. q # zp
14. a # b
15. p # q
16. u # p
17. ∃x,y:{z:Point| Colinear(z;a;b)} . (x leftof pq ∧ y leftof qp)
⊢ False
BY
{ ((Assert ab \/ pq BY
          (Unfold `geo-intersect-points` 0 THEN Auto))
   THEN (RWO "geo-intersect-points-iff2" (-1) THENA Auto)
   ) }

1
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. p : Point
5. z : Point
6. u : Point
7. q : Point
8. Colinear(u;z;p)
9. ab  ⊥u uz
10. z # ab
11. z # p
12. zp  ⊥p qp
13. q # zp
14. a # b
15. p # q
16. u # p
17. ∃x,y:{z:Point| Colinear(z;a;b)} . (x leftof pq ∧ y leftof qp)
18. a # b
∧ p # q
∧ (∃a1,b1,c,d,v:Point
    (a1-v-b1
    ∧ c-v-d
    ∧ Colinear(a1;a;b)
    ∧ Colinear(b1;a;b)
    ∧ Colinear(c;p;q)
    ∧ Colinear(d;p;q)
    ∧ a1 leftof cd
    ∧ b1 leftof dc
    ∧ c leftof b1a1
    ∧ d leftof a1b1))
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  \{b:Point|  a  \#  b\} 
4.  p  :  Point
5.  z  :  Point
6.  u  :  Point
7.  q  :  Point
8.  Colinear(u;z;p)
9.  ab    \mbot{}u  uz
10.  z  \#  ab
11.  z  \#  p
12.  zp    \mbot{}p  qp
13.  q  \#  zp
14.  a  \#  b
15.  p  \#  q
16.  u  \#  p
17.  \mexists{}x,y:\{z:Point|  Colinear(z;a;b)\}  .  (x  leftof  pq  \mwedge{}  y  leftof  qp)
\mvdash{}  False


By

---

Latex:
((Assert  ab  \mbackslash{}/  pq  BY
                (Unfold  `geo-intersect-points`  0  THEN  Auto))
  THEN  (RWO  "geo-intersect-points-iff2"  (-1)  THENA  Auto)
  )

---

Home Index