---

Step * 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 ∧ cx ≅ yx) ∧ cx ≅ cy) ∧ c # yx
9. s : c ≠ x
⊢ ¬<x, y, m2> || <c, x, s>
BY
{ (D 0 THEN Auto) }

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
13. <x, y, m2> || <c, x, s>
⊢ False

---

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  \mwedge{}  cx  \mcong{}  yx)  \mwedge{}  cx  \mcong{}  cy)  \mwedge{}  c  \#  yx
9.  s  :  c  \mneq{}  x
\mvdash{}  \mneg{}<x,  y,  m2>  ||  <c,  x,  s>


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index