let S be Subset of R; :: thesis: S is X -defined
A: dom R c= X by Def18;
dom S c= dom R by Th25;
hence dom S c= X by A, XBOOLE_1:1; :: according to RELAT_1:def 18 :: thesis: verum