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

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