---

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


1. e : EuclideanPlane
2. p : Point
3. a : Point
4. b : {b:Point| a # b} 
5. z : Point
6. q : Point
7. Colinear(p;z;p)
8. ab  ⊥p pz
9. z # p
10. zp  ⊥p qp
11. q # zp
12. a # b
13. p # q
14. ∃x,y:{z:Point| Colinear(z;a;b)} . (x leftof pq ∧ y leftof qp)
15. Rzpq
16. Colinear(a;p;q)
⊢ Colinear(a;b;q)
BY
{ (InstLemma `adjacent-right-angles` [⌜e⌝;⌜b⌝;⌜p⌝;⌜z⌝;⌜q⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:

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


By

---

Latex:
(InstLemma  `adjacent-right-angles`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index