:: deftheorem defines {} CLASSES4:def 5 :
for UN being Universe holds {} UN = {} ;