theorem :: SYSREL:9

for X, Y, Z, W being set
for R being Relation st R c= [:X,Y:] & X = Z \/ W holds
R = (R | Z) \/ (R | W)