theorem :: CLASSES4:39

for UN being Universe
for X being set
for Y being non empty set
for f being Function of X,Y st f in UN holds
X in UN