for X, Y being set
for R being Relation of X,Y holds
( dom (R ~) = rng R & rng (R ~) = dom R )