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

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