Step
*
1
of Lemma
proj-point-sep_defA
1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. x ≠ x1
⊢ ∃n:Line?. ((¬pp-sep(e;inl x;n)) ∧ pp-sep(e;inl x1;n))
BY
{ Assert ⌜∃m:Line. (x I m ∧ x1 # m)⌝⋅ }
1
.....assertion..... 
1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. x ≠ x1
⊢ ∃m:Line. (x I m ∧ x1 # m)
2
1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. x ≠ x1
5. ∃m:Line. (x I m ∧ x1 # m)
⊢ ∃n:Line?. ((¬pp-sep(e;inl x;n)) ∧ pp-sep(e;inl x1;n))
Latex:
Latex:
1.  e  :  EuclideanParPlane
2.  x  :  Point
3.  x1  :  Point
4.  x  \mneq{}  x1
\mvdash{}  \mexists{}n:Line?.  ((\mneg{}pp-sep(e;inl  x;n))  \mwedge{}  pp-sep(e;inl  x1;n))
By
Latex:
Assert  \mkleeneopen{}\mexists{}m:Line.  (x  I  m  \mwedge{}  x1  \#  m)\mkleeneclose{}\mcdot{}
Home
Index