theorem :: CLASSES4:41

for UN being Universe
for X being set st id X is Element of UN holds
X is Element of UN