let X, Y be set ; :: thesis: the_transitive-closure_of (X \/ Y) = (the_transitive-closure_of X) \/ (the_transitive-closure_of Y)
( X c= the_transitive-closure_of X & Y c= the_transitive-closure_of Y ) by Th52;
then A1: X \/ Y c= (the_transitive-closure_of X) \/ (the_transitive-closure_of Y) by XBOOLE_1:13;
the_transitive-closure_of (X \/ Y) c= the_transitive-closure_of ((the_transitive-closure_of X) \/ (the_transitive-closure_of Y)) by A1, Th58;
hence the_transitive-closure_of (X \/ Y) c= (the_transitive-closure_of X) \/ (the_transitive-closure_of Y) by Th49, Th55; :: according to XBOOLE_0:def 10 :: thesis: (the_transitive-closure_of X) \/ (the_transitive-closure_of Y) c= the_transitive-closure_of (X \/ Y)
( the_transitive-closure_of X c= the_transitive-closure_of (X \/ Y) & the_transitive-closure_of Y c= the_transitive-closure_of (X \/ Y) ) by Th58, XBOOLE_1:7;
hence (the_transitive-closure_of X) \/ (the_transitive-closure_of Y) c= the_transitive-closure_of (X \/ Y) by XBOOLE_1:8; :: thesis: verum