theorem :: RELAT_1:45

for X being set holds
( dom (id X) = X & rng (id X) = X ) ;