let X be set ; :: thesis: for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for F being Function of NAT ,S
for A being set
for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (r + (1 / (n + 1))))) ) holds
A /\ (less_eq_dom f,(R_EAL r)) = meet (rng F)
let f be PartFunc of X,ExtREAL ; :: thesis: for S being SigmaField of X
for F being Function of NAT ,S
for A being set
for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (r + (1 / (n + 1))))) ) holds
A /\ (less_eq_dom f,(R_EAL r)) = meet (rng F)
let S be SigmaField of X; :: thesis: for F being Function of NAT ,S
for A being set
for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (r + (1 / (n + 1))))) ) holds
A /\ (less_eq_dom f,(R_EAL r)) = meet (rng F)
let F be Function of NAT ,S; :: thesis: for A being set
for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (r + (1 / (n + 1))))) ) holds
A /\ (less_eq_dom f,(R_EAL r)) = meet (rng F)
let A be set ; :: thesis: for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (r + (1 / (n + 1))))) ) holds
A /\ (less_eq_dom f,(R_EAL r)) = meet (rng F)
let r be real number ; :: thesis: ( ( for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (r + (1 / (n + 1))))) ) implies A /\ (less_eq_dom f,(R_EAL r)) = meet (rng F) )
assume A1: for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (r + (1 / (n + 1))))) ; :: thesis: A /\ (less_eq_dom f,(R_EAL r)) = meet (rng F)
for x being set st x in A /\ (less_eq_dom f,(R_EAL r)) holds
x in meet (rng F)

proof

let x be set ; :: thesis: ( x in A /\ (less_eq_dom f,(R_EAL r)) implies x in meet (rng F) )
assume A3: x in A /\ (less_eq_dom f,(R_EAL r)) ; :: thesis: x in meet (rng F)
then A4: x in A by XBOOLE_0:def 4;
A5: x in less_eq_dom f,(R_EAL r) by A3, XBOOLE_0:def 4;
for Y being set st Y in rng F holds
x in Y

proof

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

proof

assume Y in rng F ; :: thesis: x in Y
then consider m being Element of NAT such that
m in dom F and
A9: Y = F . m by PARTFUN1:26;
A10: Y = A /\ (less_dom f,(R_EAL (r + (1 / (m + 1))))) by A1, A9;
A11: x in dom f by A5, Def13;
reconsider x = x as Element of X by A3;
A12: f . x <= R_EAL r by A5, Def13;
(m + 1) " > 0 ;
then 1 / (m + 1) > 0 by XCMPLX_1:217;
then R_EAL r < R_EAL (r + (1 / (m + 1))) by XREAL_1:31;
then f . x < R_EAL (r + (1 / (m + 1))) by A12, XXREAL_0:2;
then x in less_dom f,(R_EAL (r + (1 / (m + 1)))) by A11, Def12;
hence x in Y by A4, A10, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

hence x in meet (rng F) by SETFAM_1:def 1; :: thesis: verum

end;

then A18: A /\ (less_eq_dom f,(R_EAL r)) c= meet (rng F) by TARSKI:def 3;
for x being set st x in meet (rng F) holds
x in A /\ (less_eq_dom f,(R_EAL r))

proof

let x be set ; :: thesis: ( x in meet (rng F) implies x in A /\ (less_eq_dom f,(R_EAL r)) )
assume A20: x in meet (rng F) ; :: thesis: x in A /\ (less_eq_dom f,(R_EAL r))
A21: for m being Element of NAT holds
( x in A & x in dom f & f . x < R_EAL (r + (1 / (m + 1))) )

proof

let m be Element of NAT ; :: thesis: ( x in A & x in dom f & f . x < R_EAL (r + (1 / (m + 1))) )
m in NAT ;
then m in dom F by FUNCT_2:def 1;
then F . m in rng F by FUNCT_1:def 5;
then x in F . m by A20, SETFAM_1:def 1;
then A26: x in A /\ (less_dom f,(R_EAL (r + (1 / (m + 1))))) by A1;
then x in less_dom f,(R_EAL (r + (1 / (m + 1)))) by XBOOLE_0:def 4;
hence ( x in A & x in dom f & f . x < R_EAL (r + (1 / (m + 1))) ) by A26, Def12, XBOOLE_0:def 4; :: thesis: verum

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 5;
then x in F . 1 by A20, SETFAM_1:def 1;
then x in A /\ (less_dom f,(R_EAL (r + (1 / (1 + 1))))) by A1;
then reconsider x = x as Element of X ;
y <= R_EAL r

proof

now

per cases ( y = -infty or not y = -infty ) ;

suppose y = -infty ; :: thesis: y <= R_EAL r

hence y <= R_EAL r by XXREAL_0:5; :: thesis: verum

end;

suppose not y = -infty ; :: thesis: y <= R_EAL r

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

proof

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

end;

hence y <= R_EAL r by Th14; :: thesis: verum

end;

end;

end;

hence y <= R_EAL r ; :: thesis: verum

end;

then x in less_eq_dom f,(R_EAL r) by A21, Def13;
hence x in A /\ (less_eq_dom f,(R_EAL r)) by A21, XBOOLE_0:def 4; :: thesis: verum

end;

then meet (rng F) c= A /\ (less_eq_dom f,(R_EAL r)) by TARSKI:def 3;
hence A /\ (less_eq_dom f,(R_EAL r)) = meet (rng F) by A18, XBOOLE_0:def 10; :: thesis: verum