---

Step * 1 1 of Lemma Euclid-Prop31


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. a # b
6. x # ab
7. z : Point
8. u : Point
9. q : Point
10. Colinear(u;z;x)
11. ab  ⊥u uz
12. z # ab
13. z # x
14. zx  ⊥x qx
15. q # zx
⊢ ∃y:Point. geo-parallel-points(e;a;b;x;y)
BY
{ ((Assert x # q BY
          Auto)
   THEN D 0 With ⌜q⌝ 
   THEN Auto
   THEN RWO "geo-parallel-iff-not-intersect" 0
   THEN Auto
   THEN (D 0 THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. a # b
6. x # ab
7. z : Point
8. u : Point
9. q : Point
10. Colinear(u;z;x)
11. ab  ⊥u uz
12. z # ab
13. z # x
14. zx  ⊥x qx
15. q # zx
16. x # q
17. a # b
18. x # q
19. ab \/ xq
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  x  :  Point
5.  a  \#  b
6.  x  \#  ab
7.  z  :  Point
8.  u  :  Point
9.  q  :  Point
10.  Colinear(u;z;x)
11.  ab    \mbot{}u  uz
12.  z  \#  ab
13.  z  \#  x
14.  zx    \mbot{}x  qx
15.  q  \#  zx
\mvdash{}  \mexists{}y:Point.  geo-parallel-points(e;a;b;x;y)


By

---

Latex:
((Assert  x  \#  q  BY
                Auto)
  THEN  D  0  With  \mkleeneopen{}q\mkleeneclose{} 
  THEN  Auto
  THEN  RWO  "geo-parallel-iff-not-intersect"  0
  THEN  Auto
  THEN  (D  0  THENA  Auto))

---

Home Index