Step * 1 of Lemma geo-le-pt-comm


1. BasicGeometry
2. Point
3. Point
⊢ ab≤ba
BY
((Unfold `geo-le-pt` THEN InstConcl [⌜a⌝]⋅THEN Auto) }


Latex:


Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
\mvdash{}  ab\mleq{}ba


By


Latex:
((Unfold  `geo-le-pt`  0  THEN  InstConcl  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{})  THEN  Auto)




Home Index