let A, X be set ; :: thesis: for R being Relation st dom R c= X holds
R \ (R | A) = R | (X \ A)
let R be Relation; :: thesis: ( dom R c= X implies R \ (R | A) = R | (X \ A) )
assume dom R c= X ; :: thesis: R \ (R | A) = R | (X \ A)
hence R \ (R | A) = (R | X) \ (R | A) by Th62
.= R | (X \ A) by Th74 ;
:: thesis: verum