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