let X, A 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 Th97
.= R | (X \ A) by Th109 ;
:: thesis: verum