theorem Th167: :: RELAT_1:177

for A being set
for R being Relation holds dom (R \ (R | A)) = (dom R) \ A