:: deftheorem Def12 defines class CLASSES5:def 11 :
for U being Universe
for b₂ being non empty set holds
( b₂ is class of U iff b₂ is U -Class );