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