let Y be set ; :: thesis: for R being Relation holds rng (Y | R) c= rng R
let R be Relation; :: thesis: rng (Y | R) c= rng R
Y | R c= R by Th117;
hence rng (Y | R) c= rng R by Th25; :: thesis: verum