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 & R " (rng R) = dom R ) by Th167, Th169;
hence R " Y c= R " (rng R) ; :: thesis: verum