( dom (X | R) c= dom R & dom R c= A ) by Def18, Th99A;
hence dom (X | R) c= A by XBOOLE_1:1; :: according to RELAT_1:def 18 :: thesis: verum