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 Th70;
hence R c= S | (dom R) ; :: thesis: verum

end;

thus ( R c= S | (dom R) implies R c= S ) by Def9; :: thesis: verum