let X1, X2, Y1, 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 Th94;
hence [:X1,X2:] c= [:Y1,Y2:] ; :: thesis: verum