Step * of Lemma geo-incident-not-plsep

∀[e:EuclideanPlane]. ∀[x:Point]. ∀[m:Line].  ¬x # m supposing x I m
BY
{ Auto }

1
1. e : EuclideanPlane
2. x : Point
3. m : Line
4. x I m
⊢ ¬x # m


Latex:


Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[x:Point].  \mforall{}[m:Line].    \mneg{}x  \#  m  supposing  x  I  m


By


Latex:
Auto




Home Index