:: deftheorem defines universal CLASSES2:def 1 :
for IT being set holds
( IT is universal iff ( IT is epsilon-transitive & IT is Tarski ) );