theorem Th64: :: CLASSES4:64

for UN being non trivial Universe
for X being non empty set st X in UN holds
X * in UN