theorem :: CLASSES4:30

for UN being Universe
for u being Element of UN holds
( not u,UN are_equipotent & card u in card UN ) by CLASSES2:1;