let A, B, X, Y be set ; :: thesis: ( A c= X & B c= Y implies [:A,Y:] /\ [:X,B:] = [:A,B:] )
assume that
A1: A c= X and
A2: B c= Y ; :: thesis: [:A,Y:] /\ [:X,B:] = [:A,B:]
A3: [:A,Y:] /\ [:X,B:] = [:(A /\ X),(Y /\ B):] by Th99;
A /\ X = A by A1, XBOOLE_1:28;
hence [:A,Y:] /\ [:X,B:] = [:A,B:] by A2, A3, XBOOLE_1:28; :: thesis: verum