theorem Th18: :: CLASSES5:18

for U being Universe
for x being object holds
( x in U iff {x} in U )