theorem :: CLASSES5:50

for U being Universe
for x being set holds {x} is U -petit