let X be set ; :: thesis: ex A being Ordinal st X c= Rank A
consider A being Ordinal such that
A1: Tarski-Class (the_transitive-closure_of X) c= Rank A by Th47;
take A ; :: thesis: X c= Rank A
the_transitive-closure_of X in Tarski-Class (the_transitive-closure_of X) by Th2;
then X in Tarski-Class (the_transitive-closure_of X) by Th3, Th52;
hence X c= Rank A by A1, ORDINAL1:def 2; :: thesis: verum