let X be set ; :: thesis: ( X is epsilon-transitive implies Tarski-Class X is epsilon-transitive )
consider A being Ordinal such that
A1: Tarski-Class (X,A) = Tarski-Class X by Th19;
Tarski-Class (X,A) c= Tarski-Class (X,(succ A)) by Th15;
then A2: Tarski-Class (X,A) = Tarski-Class (X,(succ A)) by A1;
assume X is epsilon-transitive ; :: thesis: Tarski-Class X is epsilon-transitive
hence Tarski-Class X is epsilon-transitive by A1, A2, Th22; :: thesis: verum