let R, S be Relation; :: thesis: ( R c= S iff R c= S | (dom R) )
thus ( R c= S implies R c= S | (dom R) ) :: thesis: ( R c= S | (dom R) implies R c= S )

proof

assume R c= S ; :: thesis: R c= S | (dom R)
then R | (dom R) c= S | (dom R) by Th105;
hence R c= S | (dom R) by Th97; :: thesis: verum

end;

S | (dom R) c= S by Th88;
hence ( R c= S | (dom R) implies R c= S ) by XBOOLE_1:1; :: thesis: verum