let X, Y be set ; :: thesis: ( X c= Y implies X in the_universe_of Y )
A1: Y c= the_transitive-closure_of Y by CLASSES1:52;
Tarski-Class (the_transitive-closure_of Y) is_Tarski-Class_of the_transitive-closure_of Y by CLASSES1:def 4;
then A2: the_transitive-closure_of Y in Tarski-Class (the_transitive-closure_of Y) by CLASSES1:def 3;
assume X c= Y ; :: thesis: X in the_universe_of Y
then X c= the_transitive-closure_of Y by A1;
hence X in the_universe_of Y by A2, CLASSES1:def 1; :: thesis: verum