let X be set ; :: thesis: ( X is epsilon-transitive implies Tarski-Class X is universal )
assume X is epsilon-transitive ; :: thesis: Tarski-Class X is universal
hence ( Tarski-Class X is epsilon-transitive & Tarski-Class X is Tarski ) by CLASSES1:27; :: according to CLASSES2:def 1 :: thesis: verum