let Y be set ; :: thesis: for R being Relation holds rng (Y |` R) = (rng R) /\ Y
let R be Relation; :: thesis: rng (Y |` R) = (rng R) /\ Y
( rng (Y |` R) c= Y & rng (Y |` R) c= rng R ) by Th85, Th87;
hence rng (Y |` R) c= (rng R) /\ Y by XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis: (rng R) /\ Y c= rng (Y |` R)
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (rng R) /\ Y or y in rng (Y |` R) )
assume A1: y in (rng R) /\ Y ; :: thesis: y in rng (Y |` R)
then y in rng R by XBOOLE_0:def 4;
then consider x being set such that
A2: [x,y] in R by XTUPLE_0:def 13;
y in Y by A1, XBOOLE_0:def 4;
then [x,y] in Y |` R by A2, Def12;
hence y in rng (Y |` R) by XTUPLE_0:def 13; :: thesis: verum