let Y be set ; :: thesis: for R being Relation st Y c= rng R holds
rng (Y | R) = Y
let R be Relation; :: thesis: ( Y c= rng R implies rng (Y | R) = Y )
assume Y c= rng R ; :: thesis: rng (Y | R) = Y
then (rng R) /\ Y = Y by XBOOLE_1:28;
hence rng (Y | R) = Y by Th119; :: thesis: verum