let X be set ; :: thesis: for R being Relation st X c= dom R holds
dom (R | X) = X
let R be Relation; :: thesis: ( X c= dom R implies dom (R | X) = X )
( dom (R | X) = (dom R) /\ X & ( X c= dom R implies (dom R) /\ X = X ) ) by Th90, XBOOLE_1:28;
hence ( X c= dom R implies dom (R | X) = X ) ; :: thesis: verum