let A be set ; :: thesis: for R being Relation holds dom (R \ (R | A)) = (dom R) \ A
let R be Relation; :: thesis: dom (R \ (R | A)) = (dom R) \ A
R \ (R | A) = R | ((dom R) \ A) by Th166;
hence dom (R \ (R | A)) = (dom R) /\ ((dom R) \ A) by Th55
.= ((dom R) /\ (dom R)) \ A by XBOOLE_1:49
.= (dom R) \ A ;
:: thesis: verum