let X, Y be set ; :: thesis: the_transitive-closure_of (X /\ Y) c= (the_transitive-closure_of X) /\ (the_transitive-closure_of Y)
( the_transitive-closure_of (X /\ Y) c= the_transitive-closure_of X & the_transitive-closure_of (X /\ Y) c= the_transitive-closure_of Y ) by Th58, XBOOLE_1:17;
hence the_transitive-closure_of (X /\ Y) c= (the_transitive-closure_of X) /\ (the_transitive-closure_of Y) by XBOOLE_1:19; :: thesis: verum