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 /\ (great_dom (f,(R_EAL (r - (1 / (m + 1)))))) by A1, A5;
A7: x in dom f by A4, Def15;
reconsider x = x as Element of X by A2;
A8: R_EAL r <= f . x by A4, Def15;
(m + 1) " > 0 ;
then 1 / (m + 1) > 0 by XCMPLX_1:215;
then r < r + (1 / (m + 1)) by XREAL_1:29;
then R_EAL (r - (1 / (m + 1))) < R_EAL r by XREAL_1:19;
then R_EAL (r - (1 / (m + 1))) < f . x by A8, XXREAL_0:2;
then x in great_dom (f,(R_EAL (r - (1 / (m + 1))))) by A7, Def14;
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 set ; :: thesis:
assume A10: x in meet (rng F) ; :: thesis:
A11: for m being Element of NAT holds
( x in A & x in dom f & R_EAL (r - (1 / (m + 1))) < f . x )

end;

reconsider y = f . x as R_eal ;
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 /\ (great_dom (f,(R_EAL (r - (1 / (1 + 1)))))) by A1;
then reconsider x = x as Element of X ;
R_EAL r <= y

end;

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

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

end;

end;

end;

end;