theorem :: CLASSES5:30

for U being Universe
for X being Set of U holds U \ X is class of U