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