A1: dom (R \/ S) = (dom R) \/ (dom S) by XTUPLE_0:23;
( dom R c= X & dom S c= X ) by RELAT_1:def 18;
hence dom (R \/ S) c= X by A1, XBOOLE_1:8; :: according to RELAT_1:def 18 :: thesis: verum