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