theorem :: SYSREL:20

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