let A, X, B, Y be set ; :: thesis: ( A c= X & B c= Y implies [:A,Y:] /\ [:X,B:] = [:A,B:] )
assume ( A c= X & B c= Y ) ; :: thesis: [:A,Y:] /\ [:X,B:] = [:A,B:]
then ( [:A,Y:] /\ [:X,B:] = [:(A /\ X),(Y /\ B):] & A /\ X = A & Y /\ B = B ) by Th123, XBOOLE_1:28;
hence [:A,Y:] /\ [:X,B:] = [:A,B:] ; :: thesis: verum