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 RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in [:Y,Z:] or [x,b₁] in Tarski-Class X )
let y be set ; :: 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, Th31; :: thesis: verum