let X, Y be set ; :: thesis: ( X c= Y implies the_transitive-closure_of X c= the_transitive-closure_of Y )
assume A1: X c= Y ; :: thesis: the_transitive-closure_of X c= the_transitive-closure_of Y
Y c= the_transitive-closure_of Y by Th52;
then X c= the_transitive-closure_of Y by A1;
hence the_transitive-closure_of X c= the_transitive-closure_of Y by Th53; :: thesis: verum