Step * 4 2 of Lemma projective-points-exist


1. EuclideanParPlane
2. Unit
3. y1 Unit
4. Line
⊢ ¬¬(∃p:Point Line. ((¬pp-sep(e;p;inr )) ∧ pp-sep(e;p;inr y1 ))))
BY
(RenameVar `l' (-1) THEN (RemoveDoubleNegation THENA Auto)) }

1
1. EuclideanParPlane
2. Unit
3. y1 Unit
4. Line
⊢ ∃p:Point Line. ((¬pp-sep(e;p;inr )) ∧ 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