let Y be set ; :: thesis: for R being Relation holds R " Y c= R " (rng R)
let R be Relation; :: thesis: R " Y c= R " (rng R)
R " Y c= dom R by Th167;
hence R " Y c= R " (rng R) by Th169; :: thesis: verum