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 Th22;
A2: Tarski-Class X,A c= Tarski-Class X,(succ A) by Th18;
A3: Tarski-Class X,A = Tarski-Class X,(succ A) by A1, A2, XBOOLE_0:def 10;
assume A4: X is epsilon-transitive ; :: thesis: Tarski-Class X is epsilon-transitive
thus Tarski-Class X is epsilon-transitive by A1, A3, A4, Th25; :: thesis: verum