let X be set ; for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for F being sequence of S
for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
A /\ (less_eq_dom (f,r)) = meet (rng F)
let f be PartFunc of X,ExtREAL; for S being SigmaField of X
for F being sequence of S
for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
A /\ (less_eq_dom (f,r)) = meet (rng F)
let S be SigmaField of X; for F being sequence of S
for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
A /\ (less_eq_dom (f,r)) = meet (rng F)
let F be sequence of S; for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
A /\ (less_eq_dom (f,r)) = meet (rng F)
let A be set ; for r being Real st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
A /\ (less_eq_dom (f,r)) = meet (rng F)
let r be Real; ( ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(r + (1 / (n + 1))))) ) implies A /\ (less_eq_dom (f,r)) = meet (rng F) )
assume A1:
for n being Element of NAT holds F . n = A /\ (less_dom (f,(r + (1 / (n + 1)))))
; A /\ (less_eq_dom (f,r)) = meet (rng F)
for x being object st x in A /\ (less_eq_dom (f,r)) holds
x in meet (rng F)
then A9:
A /\ (less_eq_dom (f,r)) c= meet (rng F)
;
for x being object st x in meet (rng F) holds
x in A /\ (less_eq_dom (f,r))
then
meet (rng F) c= A /\ (less_eq_dom (f,r))
;
hence
A /\ (less_eq_dom (f,r)) = meet (rng F)
by A9, XBOOLE_0:def 10; verum