( dom R c= X & dom (R \ S) c= dom R ) by RELAT_1:25, RELAT_1:def 18;
hence dom (R \ S) c= X by XBOOLE_1:1; :: according to RELAT_1:def 18 :: thesis: verum