theorem Th14: :: RELAT_1:20
for R being Relation holds
( rng R = dom (R ~) & dom R = rng (R ~) )