---

Step * 1 1 1 1 2 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 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)
BY
{ (((gProperProlong ⌜y⌝⌜x⌝`y\''⌜y⌝⌜x⌝⋅ THEN Auto) THEN InstConcl [⌜y⌝;⌜y'⌝]⋅)
   THEN Auto
   THEN D 16
   THEN InstLemma `left-between-implies-right1` [⌜eu⌝;⌜c⌝;⌜x⌝;⌜y⌝;⌜y'⌝]⋅
   THEN Auto) }

---

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  leftof  xy
12.  s  :  c  \mneq{}  x
13.  x  leftof  yc
14.  y  leftof  cx
\mvdash{}  \mexists{}a,b:Point.  (Colinear(a;x;y)  \mwedge{}  Colinear(b;x;y)  \mwedge{}  a  leftof  cx  \mwedge{}  b  leftof  xc)


By

---

Latex:
(((gProperProlong  \mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}`y\mbackslash{}''\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  InstConcl  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}y'\mkleeneclose{}]\mcdot{})
  THEN  Auto
  THEN  D  16
  THEN  InstLemma  `left-between-implies-right1`  [\mkleeneopen{}eu\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}y'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index