let X, Y, Z be set ; :: thesis: ( Y c= the_universe_of X & Z c= the_universe_of X implies [:Y,Z:] c= the_universe_of X )
assume Y c= the_universe_of X ; :: thesis: ( not Z c= the_universe_of X or [:Y,Z:] c= the_universe_of X )
then A1: Y c= Tarski-Class (the_transitive-closure_of X) by YELLOW_6:def 3;
assume Z c= the_universe_of X ; :: thesis: [:Y,Z:] c= the_universe_of X
then A2: Z c= Tarski-Class (the_transitive-closure_of X) by YELLOW_6:def 3;
[:Y,Z:] c= Tarski-Class (the_transitive-closure_of X) by A1, A2, CLASSES1:32;
hence [:Y,Z:] c= the_universe_of X by YELLOW_6:def 3; :: thesis: verum