R " A c= dom R by RELAT_1:132;
hence R " A is Subset of X by XBOOLE_1:1; :: thesis: verum