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
A2: Y c= the_transitive-closure_of Y by Th59;
A3: X c= the_transitive-closure_of Y by A1, A2, XBOOLE_1:1;
thus the_transitive-closure_of X c= the_transitive-closure_of Y by A3, Th58, Th60; :: thesis: verum