Step
*
of Lemma
le_reflexive
∀a:ℤ. (a ≤ a)
BY
{ ((UnivCD THENA Auto) THEN BLemma `le_weakening` THEN Auto) }
Latex:
Latex:
\mforall{}a:\mBbbZ{}.  (a  \mleq{}  a)
By
Latex:
((UnivCD  THENA  Auto)  THEN  BLemma  `le\_weakening`  THEN  Auto)
Home
Index