Step * of Lemma eu-lt-null-segment

e:EuclideanPlane. ∀[p:{p:Point| O_X_p} ]. ∀[a:Point].  uiff(p < |aa|;False)
BY
((UnivCD THENA Auto) THEN Unfold `eu-lt` THEN RWO "eu-le-null-segment" THEN Auto) }


Latex:


Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[p:\{p:Point|  O\_X\_p\}  ].  \mforall{}[a:Point].    uiff(p  <  |aa|;False)


By


Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `eu-lt`  0  THEN  RWO  "eu-le-null-segment"  0  THEN  Auto)




Home Index