theorem :: CLASSES4:80

for UN1, UN2 being Universe
for a being Element of UN1 st not a in UN2 holds
UN2 in UN1