theorem :: CLASSES5:48

for U being Universe
for X being Element of U holds X is U -petit ;