let y, Y be set ; :: thesis: for R being Relation holds
( y in rng (Y | R) iff ( y in Y & y in rng R ) )
let R be Relation; :: thesis: ( y in rng (Y | R) iff ( y in Y & y in rng R ) )
thus ( y in rng (Y | R) implies ( y in Y & y in rng R ) ) :: thesis: ( y in Y & y in rng R implies y in rng (Y | R) )

proof

assume y in rng (Y | R) ; :: thesis: ( y in Y & y in rng R )
then consider x being set such that
A1: [x,y] in Y | R by Def5;
( [x,y] in R & y in Y ) by A1, Def12;
hence ( y in Y & y in rng R ) by Def5; :: thesis: verum

end;

assume A2: y in Y ; :: thesis: ( not y in rng R or y in rng (Y | R) )
assume y in rng R ; :: thesis: y in rng (Y | R)
then consider x being set such that
A3: [x,y] in R by Def5;
[x,y] in Y | R by A2, A3, Def12;
hence y in rng (Y | R) by Def5; :: thesis: verum