let X, Y be set ; :: thesis: the_transitive-closure_of (X /\ Y) c= (the_transitive-closure_of X) /\ (the_transitive-closure_of Y)
A1: ( 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 Th65, XBOOLE_1:17;
thus the_transitive-closure_of (X /\ Y) c= (the_transitive-closure_of X) /\ (the_transitive-closure_of Y) by A1, XBOOLE_1:19; :: thesis: verum