---

Step * 1 1 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 leftof yx
12. s : c ≠ x
13. y leftof xc
14. x leftof cy
15. y' : Point
16. y-x-y'
17. xy' ≅ yx
18. Colinear(y';x;y)
19. Colinear(y;x;y)
⊢ y' leftof cx
BY
{ (D 16 THEN InstLemma `left-between-implies-right2` [⌜eu⌝;⌜x⌝;⌜c⌝;⌜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  yx
12.  s  :  c  \mneq{}  x
13.  y  leftof  xc
14.  x  leftof  cy
15.  y'  :  Point
16.  y-x-y'
17.  xy'  \mcong{}  yx
18.  Colinear(y';x;y)
19.  Colinear(y;x;y)
\mvdash{}  y'  leftof  cx


By

---

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

---

Home Index