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