theorem :: CLASSES2:57

for x being set
for U being Universe st x in U holds
{x} in U by Th2;