let X, Y, 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, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in [:Y,Z:] or [x,y] in Tarski-Class X )
assume [x,y] in [:Y,Z:] ; :: thesis: [x,y] in Tarski-Class X
then ( x in Y & y in Z ) by ZFMISC_1:87;
hence [x,y] in Tarski-Class X by A1, Th27; :: thesis: verum