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 Th86;
hence rng (Y |` R) c= rng R by Th11; :: thesis: verum