theorem :: CLASSES1:61

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