---

Step * 1 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
⊢ <x, y, m2> \/ <c, x, s>
BY
{ ((RWO "geo-intersect-lines" 0 THENA Auto)
   THEN Reduce 0
   THEN D -2
   THEN FLemma `left-symmetry` [-2]
   THEN Auto
   THEN (FLemma `left-symmetry` [-1] THENA 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 leftof yx
12. s : c ≠ x
13. y leftof xc
14. x leftof cy
⊢ ∃a,b:Point. (Colinear(a;x;y) ∧ Colinear(b;x;y) ∧ a leftof cx ∧ b leftof xc)

2
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 leftof xy
12. s : c ≠ x
13. x leftof yc
14. y leftof cx
⊢ ∃a,b:Point. (Colinear(a;x;y) ∧ Colinear(b;x;y) ∧ a leftof cx ∧ b leftof xc)

---

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
\mvdash{}  <x,  y,  m2>  \mbackslash{}/  <c,  x,  s>


By

---

Latex:
((RWO  "geo-intersect-lines"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  D  -2
  THEN  FLemma  `left-symmetry`  [-2]
  THEN  Auto
  THEN  (FLemma  `left-symmetry`  [-1]  THENA  Auto))

---

Home Index