:: deftheorem Def6 defines trivial CLASSES4:def 6 :
for UN being Universe holds
( UN is trivial iff not omega in UN );