Step
*
4
2
of Lemma
projective-points-exist
1. e : EuclideanParPlane
2. y : Unit
3. y1 : Unit
4. Line
⊢ ¬¬(∃p:Point + Line. ((¬pp-sep(e;p;inr y )) ∧ (¬pp-sep(e;p;inr y1 ))))
BY
{ (RenameVar `l' (-1) THEN (RemoveDoubleNegation THENA Auto)) }
1
1. e : EuclideanParPlane
2. y : Unit
3. y1 : Unit
4. l : Line
⊢ ∃p:Point + Line. ((¬pp-sep(e;p;inr y )) ∧ (¬pp-sep(e;p;inr y1 )))
Latex:
Latex:
1.  e  :  EuclideanParPlane
2.  y  :  Unit
3.  y1  :  Unit
4.  Line
\mvdash{}  \mneg{}\mneg{}(\mexists{}p:Point  +  Line.  ((\mneg{}pp-sep(e;p;inr  y  ))  \mwedge{}  (\mneg{}pp-sep(e;p;inr  y1  ))))
By
Latex:
(RenameVar  `l'  (-1)  THEN  (RemoveDoubleNegation  THENA  Auto))
Home
Index