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 1;
assume Z c= the_universe_of X ; :: thesis: [:Y,Z:] c= the_universe_of X
then Z c= Tarski-Class (the_transitive-closure_of X) by YELLOW_6:def 1;
then [:Y,Z:] c= Tarski-Class (the_transitive-closure_of X) by A1, CLASSES1:28;
hence [:Y,Z:] c= the_universe_of X by YELLOW_6:def 1; :: thesis: verum