theorem :: CLASSES4:29

for UN being Universe
for u being Element of UN holds card u in UN by CLASSES2:11;