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 Th84; :: thesis: verum