---

Step * 1 1 1 of Lemma p_inf-l_eu-sep-exists


1. eu : EuclideanParPlane
2. p : l,m:Line//l || m
3. x : Point
4. y : Point
5. m2 : x ≠ y
6. <x, y, m2> = p ∈ (l,m:Line//l || m)
7. c : Point
8. cy ≅ xy
9. cx ≅ yx
10. cx ≅ cy
11. c # yx
12. s : c ≠ x
13. <x, y, m2> || <c, x, s>
⊢ False
BY
{ (Unfold `geo-Aparallel` -1 THEN D -1) }

1
1. eu : EuclideanParPlane
2. p : l,m:Line//l || m
3. x : Point
4. y : Point
5. m2 : x ≠ y
6. <x, y, m2> = p ∈ (l,m:Line//l || m)
7. c : Point
8. cy ≅ xy
9. cx ≅ yx
10. cx ≅ cy
11. c # yx
12. s : c ≠ x
⊢ <x, y, m2> \/ <c, x, s>

---

Latex:

---

Latex:

1.  eu  :  EuclideanParPlane
2.  p  :  l,m:Line//l  ||  m
3.  x  :  Point
4.  y  :  Point
5.  m2  :  x  \mneq{}  y
6.  <x,  y,  m2>  =  p
7.  c  :  Point
8.  cy  \mcong{}  xy
9.  cx  \mcong{}  yx
10.  cx  \mcong{}  cy
11.  c  \#  yx
12.  s  :  c  \mneq{}  x
13.  <x,  y,  m2>  ||  <c,  x,  s>
\mvdash{}  False


By

---

Latex:
(Unfold  `geo-Aparallel`  -1  THEN  D  -1)

---

Home Index