theorem :: RELAT_1:178

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