for X, Y being set
for R being Relation holds
( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )