theorem Th166: :: RELAT_1:176

for A, X being set
for R being Relation st dom R c= X holds
R \ (R | A) = R | (X \ A)