let Y, X, Z be set ; :: thesis: ( Y c= Tarski-Class X & Z c= Tarski-Class X implies [:Y,Z:] c= Tarski-Class X )
assume A1: ( Y c= Tarski-Class X & Z c= Tarski-Class X ) ; :: thesis: [:Y,Z:] c= Tarski-Class X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:Y,Z:] or x in Tarski-Class X )
assume A2: x in [:Y,Z:] ; :: thesis: x in Tarski-Class X
then A3: x = [(x `1 ),(x `2 )] by MCART_1:23;
( x `1 in Y & x `2 in Z ) by A2, MCART_1:10;
hence x in Tarski-Class X by A1, A3, Th31; :: thesis: verum