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 Th59;
then ( X c= the_transitive-closure_of Y & the_transitive-closure_of Y is epsilon-transitive ) by A1, Th58, XBOOLE_1:1;
hence the_transitive-closure_of X c= the_transitive-closure_of Y by Th60; :: thesis: verum