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 Th21, Th124;
hence Y | R = R by A1, XBOOLE_1:1, XBOOLE_1:28; :: thesis: verum