for R being Relation
for X being set holds
( (R | X) ~ = X |` (R ~) & (X |` R) ~ = (R ~) | X )