let X, Y be set ; :: thesis: the_transitive-closure_of (X \/ Y) = (the_transitive-closure_of X) \/ (the_transitive-closure_of Y)
A1: ( X c= the_transitive-closure_of X & Y c= the_transitive-closure_of Y ) by Th59;
A2: X \/ Y c= (the_transitive-closure_of X) \/ (the_transitive-closure_of Y) by A1, XBOOLE_1:13;
A3: ( the_transitive-closure_of X is epsilon-transitive & the_transitive-closure_of Y is epsilon-transitive ) by Th58;
A4: the_transitive-closure_of (X \/ Y) c= the_transitive-closure_of ((the_transitive-closure_of X) \/ (the_transitive-closure_of Y)) by A2, Th65;
thus the_transitive-closure_of (X \/ Y) c= (the_transitive-closure_of X) \/ (the_transitive-closure_of Y) by A3, A4, Th55, Th62; :: according to XBOOLE_0:def 10 :: thesis: (the_transitive-closure_of X) \/ (the_transitive-closure_of Y) c= the_transitive-closure_of (X \/ Y)
A5: ( 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 Th65, XBOOLE_1:7;
thus (the_transitive-closure_of X) \/ (the_transitive-closure_of Y) c= the_transitive-closure_of (X \/ Y) by A5, XBOOLE_1:8; :: thesis: verum