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