for R being Relation st R is reflexive holds
( dom R = dom (R ~) & rng R = rng (R ~) )