theorem :: CLASSES5:49

for U being Universe
for x being set holds
( x is U -petit iff card x in card U )