let Y be set ; :: thesis: for R being Relation holds rng (Y | R) c= Y
let R be Relation; :: thesis: rng (Y | R) c= Y
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Y | R) or y in Y )
thus ( not y in rng (Y | R) or y in Y ) by Th115; :: thesis: verum