for X, Y being set holds the_transitive-closure_of (X \/ Y) = (the_transitive-closure_of X) \/ (the_transitive-closure_of Y)