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