R /\ S c= R
by XBOOLE_1:17;

then ( rng R c= X & rng (R /\ S) c= rng R ) by RELAT_1:11, RELAT_1:def 19;

hence rng (R /\ S) c= X ; :: according to RELAT_1:def 19 :: thesis: verum

then ( rng R c= X & rng (R /\ S) c= rng R ) by RELAT_1:11, RELAT_1:def 19;

hence rng (R /\ S) c= X ; :: according to RELAT_1:def 19 :: thesis: verum