theorem Th17: :: ZF_REFLE:17

NAT , VAR are_equipotent