let Y be set ; :: thesis: for R being Relation st rng R c= Y holds
Y |` R = R
let R be Relation; :: thesis: ( rng R c= Y implies Y |` R = R )
assume rng R c= Y ; :: thesis: Y |` R = R
then A1: [:(dom R),(rng R):] c= [:(dom R),Y:] by ZFMISC_1:95;
( R c= [:(dom R),(rng R):] & Y |` R = R /\ [:(dom R),Y:] ) by Th1, Th87;
hence Y |` R = R by A1, XBOOLE_1:1, XBOOLE_1:28; :: thesis: verum