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 Th124;
hence R " Y c= R " (rng R) by Th126; :: thesis: verum