let X1, Y1, X2, Y2 be set ; :: thesis: ( X1 c= Y1 & X2 c= Y2 implies [:X1,X2:] c= [:Y1,Y2:] )
assume ( X1 c= Y1 & X2 c= Y2 ) ; :: thesis: [:X1,X2:] c= [:Y1,Y2:]
then ( [:X1,X2:] c= [:Y1,X2:] & [:Y1,X2:] c= [:Y1,Y2:] ) by Th118;
hence [:X1,X2:] c= [:Y1,Y2:] by XBOOLE_1:1; :: thesis: verum