Step
*
1
of Lemma
equipollent-product-one
.....assertion..... 
ℕ1 ~ Top
BY
{ TACTIC:(RWO "top-equipollent-unit" 0 THEN Auto) }
1
ℕ1 ~ Unit
Latex:
Latex:
.....assertion..... 
\mBbbN{}1  \msim{}  Top
By
Latex:
TACTIC:(RWO  "top-equipollent-unit"  0  THEN  Auto)
Home
Index