---

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


1. eu : EuclideanParPlane
2. p : l,m:Line//l || m
3. m : Line
4. m = p ∈ (l,m:Line//l || m)
⊢ ∃L:Line. (¬m || L)
BY
{ ((((D 3 THEN D 4) THEN InstLemma `Euclid-Prop1` [⌜eu⌝;⌜x⌝;⌜y⌝]⋅) THENA Auto)
   THEN ExRepD
   THEN Unfold `geo-equilateral` -1
   THEN (Assert c ≠ x BY
               Auto)
   THEN RenameVar `s' (-1)
   THEN (InstConcl [⌜<c, x, s>⌝]⋅ 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 ∧ cx ≅ yx) ∧ cx ≅ cy) ∧ c # yx
9. s : c ≠ x
⊢ ¬<x, y, m2> || <c, x, s>

---

Latex:

---

Latex:

1.  eu  :  EuclideanParPlane
2.  p  :  l,m:Line//l  ||  m
3.  m  :  Line
4.  m  =  p
\mvdash{}  \mexists{}L:Line.  (\mneg{}m  ||  L)


By

---

Latex:
((((D  3  THEN  D  4)  THEN  InstLemma  `Euclid-Prop1`  [\mkleeneopen{}eu\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{})  THENA  Auto)
  THEN  ExRepD
  THEN  Unfold  `geo-equilateral`  -1
  THEN  (Assert  c  \mneq{}  x  BY
                          Auto)
  THEN  RenameVar  `s'  (-1)
  THEN  (InstConcl  [\mkleeneopen{}<c,  x,  s>\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index