R .: A c= rng R by RELAT_1:111;
hence R .: A is Subset of Y by XBOOLE_1:1; :: thesis: verum