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