theorem :: CLASSES4:18

for UN being Universe holds
( NAT in UN or NAT ,UN are_equipotent )