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 Th116, Th118;
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 A2: 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
A3: [x,y] in R by Def5;
y in Y by A2, XBOOLE_0:def 4;
then [x,y] in Y | R by A3, Def12;
hence y in rng (Y | R) by Def5; :: thesis: verum