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 - (1 / (m + 1))))) by A1, A5;
A7: x in dom f by A4, Def14;
reconsider x = x as Element of X by A2;
A8: r <= f . x by A4, Def14;
(m + 1) " > 0 ;
then 1 / (m + 1) > 0 by XCMPLX_1:215;
then r < r + (1 / (m + 1)) by XREAL_1:29;
then r - (1 / (m + 1)) < r by XREAL_1:19;
then r - (1 / (m + 1)) < f . x by A8, XXREAL_0:2;
then x in great_dom (f,(r - (1 / (m + 1)))) by A7, Def13;
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 & r - (1 / (m + 1)) < f . x )

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

end;

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

end;

end;

end;