Step
*
1
of Lemma
finite-unit
Unit ~ ℕ1
BY
{ ((Symmetry THEN Auto) THEN BLemma `equipollent-unit` THEN Auto) }
1
ℕ1
Latex:
Latex:
Unit  \msim{}  \mBbbN{}1
By
Latex:
((Symmetry  THEN  Auto)  THEN  BLemma  `equipollent-unit`  THEN  Auto)
Home
Index