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

proof

let x be set ; :: thesis: ( x in A /\ (great_eq_dom f,(R_EAL r)) implies x in meet (rng F) )
assume A3: x in A /\ (great_eq_dom f,(R_EAL r)) ; :: thesis: x in meet (rng F)
A4: x in A by A3, XBOOLE_0:def 4;
A5: x in great_eq_dom f,(R_EAL r) by A3, XBOOLE_0:def 4;
A6: 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 )
A7: ( Y in rng F implies x in Y )

proof

assume A8: Y in rng F ; :: thesis: x in Y
consider m being Element of NAT such that
m in dom F and
A9: Y = F . m by A8, PARTFUN1:26;
A10: Y = A /\ (great_dom f,(R_EAL (r - (1 / (m + 1))))) by A1, A9;
A11: x in dom f by A5, Def15;
reconsider x = x as Element of X by A3;
A12: R_EAL r <= f . x by A5, Def15;
A13: (m + 1) " > 0 ;
A14: 1 / (m + 1) > 0 by A13, XCMPLX_1:217;
A15: r < r + (1 / (m + 1)) by A14, XREAL_1:31;
A16: R_EAL (r - (1 / (m + 1))) < R_EAL r by A15, XREAL_1:21;
A17: R_EAL (r - (1 / (m + 1))) < f . x by A12, A16, XXREAL_0:2;
A18: x in great_dom f,(R_EAL (r - (1 / (m + 1)))) by A11, A17, Def14;
thus x in Y by A4, A10, A18, XBOOLE_0:def 4; :: thesis: verum

end;

thus ( Y in rng F implies x in Y ) by A7; :: thesis: verum

end;

thus x in meet (rng F) by A6, SETFAM_1:def 1; :: thesis: verum

end;

A19: A /\ (great_eq_dom f,(R_EAL r)) c= meet (rng F) by A2, TARSKI:def 3;
A20: for x being set st x in meet (rng F) holds
x in A /\ (great_eq_dom f,(R_EAL r))

proof

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

proof

let m be Element of NAT ; :: thesis: ( x in A & x in dom f & R_EAL (r - (1 / (m + 1))) < f . x )
A23: m in NAT ;
A24: m in dom F by A23, FUNCT_2:def 1;
A25: F . m in rng F by A24, FUNCT_1:def 5;
A26: x in F . m by A21, A25, SETFAM_1:def 1;
A27: x in A /\ (great_dom f,(R_EAL (r - (1 / (m + 1))))) by A1, A26;
A28: x in great_dom f,(R_EAL (r - (1 / (m + 1)))) by A27, XBOOLE_0:def 4;
thus ( x in A & x in dom f & R_EAL (r - (1 / (m + 1))) < f . x ) by A27, A28, Def14, XBOOLE_0:def 4; :: thesis: verum

end;

reconsider y = f . x as R_eal ;
A29: 1 in NAT ;
A30: 1 in dom F by A29, FUNCT_2:def 1;
A31: F . 1 in rng F by A30, FUNCT_1:def 5;
A32: x in F . 1 by A21, A31, SETFAM_1:def 1;
A33: x in A /\ (great_dom f,(R_EAL (r - (1 / (1 + 1))))) by A1, A32;
reconsider x = x as Element of X by A33;
A34: R_EAL r <= y

proof

A35: now

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

suppose A36: y = +infty ; :: thesis: R_EAL r <= y

thus R_EAL r <= y by A36, XXREAL_0:4; :: thesis: verum

end;

suppose A37: not y = +infty ; :: thesis: R_EAL r <= y

A38: not +infty <= y by A37, XXREAL_0:4;
A39: R_EAL (r - (1 / (1 + 1))) < y by A22;
reconsider y1 = y as Real by A38, A39, XXREAL_0:48;
A40: for m being Element of NAT holds r - (1 / (m + 1)) <= y1

proof

let m be Element of NAT ; :: thesis: r - (1 / (m + 1)) <= y1
A41: R_EAL (r - (1 / (m + 1))) < R_EAL y1 by A22;
thus r - (1 / (m + 1)) <= y1 by A41; :: thesis: verum

end;

thus R_EAL r <= y by A40, Th14; :: thesis: verum

end;

end;

end;

thus R_EAL r <= y by A35; :: thesis: verum

end;

A42: x in great_eq_dom f,(R_EAL r) by A22, A34, Def15;
thus x in A /\ (great_eq_dom f,(R_EAL r)) by A22, A42, XBOOLE_0:def 4; :: thesis: verum

end;

A43: meet (rng F) c= A /\ (great_eq_dom f,(R_EAL r)) by A20, TARSKI:def 3;
thus A /\ (great_eq_dom f,(R_EAL r)) = meet (rng F) by A19, A43, XBOOLE_0:def 10; :: thesis: verum