let X be set ; :: thesis: ex A being Ordinal st Tarski-Class (X,A) = Tarski-Class X
consider A being Ordinal such that
A1: Tarski-Class (X,A) = Tarski-Class (X,(succ A)) by Th17;
take A ; :: thesis: Tarski-Class (X,A) = Tarski-Class X
thus Tarski-Class (X,A) = Tarski-Class X by A1, Th18; :: thesis: verum