let Y be set ; :: thesis:
( Y in rng F implies x in Y )

assume Y in rng F ; :: thesis:
then consider m being Element of NAT such that
m in dom F and
A5: Y = F . m by PARTFUN1:3;
A6: Y = A /\ (less_dom (f,(r + (1 / (m + 1))))) by A1, A5;
A7: x in dom f by A4, Def12;
reconsider x = x as Element of X by A2;
A8: f . x <= r by A4, Def12;
(m + 1) " > 0 ;
then 1 / (m + 1) > 0 by XCMPLX_1:215;
then r < r + (1 / (m + 1)) by XREAL_1:29;
then f . x < r + (1 / (m + 1)) by A8, XXREAL_0:2;
then x in less_dom (f,(r + (1 / (m + 1)))) by A7, Def11;
hence x in Y by A3, A6, XBOOLE_0:def 4; :: thesis:

end;

hence ( Y in rng F implies x in Y ) ; :: thesis:

end;

end;

let x be object ; :: thesis:
assume A10: x in meet (rng F) ; :: thesis:
A11: for m being Element of NAT holds
( x in A & x in dom f & f . x < r + (1 / (m + 1)) )

end;

reconsider y = f . x as R_eal by XXREAL_0:def 1;
1 in NAT ;
then 1 in dom F by FUNCT_2:def 1;
then F . 1 in rng F by FUNCT_1:def 3;
then x in F . 1 by A10, SETFAM_1:def 1;
then x in A /\ (less_dom (f,(r + (1 / (1 + 1))))) by A1;
then reconsider x = x as Element of X ;
y <= r

end;

then A13: not y <= -infty by XXREAL_0:6;
y < r + (1 / (1 + 1)) by A11;
then reconsider y1 = y as Element of REAL by A13, XXREAL_0:48;
for m being Element of NAT holds y1 - (1 / (m + 1)) <= r

let m be Element of NAT ; :: thesis:
y1 < r + (1 / (m + 1)) by A11;
hence y1 - (1 / (m + 1)) <= r by XREAL_1:20; :: thesis:

end;

end;

end;

end;