theorem Th1: :: ALGSTR_4:1

for X, Y, Z being set st Y c= the_universe_of X & Z c= the_universe_of X holds
[:Y,Z:] c= the_universe_of X