set X = the set ;
take V = Tarski-Class (the_transitive-closure_of the set ); :: thesis: ( V is universal & not V is empty )
thus V is epsilon-transitive by CLASSES1:23; :: according to CLASSES2:def 1 :: thesis: ( V is Tarski & not V is empty )
thus ( V is Tarski & not V is empty ) ; :: thesis: verum