for A, B, X, Y being set st A c= X & B c= Y holds
[:A,Y:] /\ [:X,B:] = [:A,B:]