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