let x be object ; :: thesis: for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds
( x in lim_inf S iff ex n being Nat st
for k being Nat holds x in S . (n + k) )
let X be set ; :: thesis: for Si being SigmaField of X
for S being SetSequence of Si holds
( x in lim_inf S iff ex n being Nat st
for k being Nat holds x in S . (n + k) )
let Si be SigmaField of X; :: thesis: for S being SetSequence of Si holds
( x in lim_inf S iff ex n being Nat st
for k being Nat holds x in S . (n + k) )
let S be SetSequence of Si; :: thesis: ( x in lim_inf S iff ex n being Nat st
for k being Nat holds x in S . (n + k) )
for B being SetSequence of X holds
( x in Union (inferior_setsequence B) iff ex n being Nat st
for k being Nat holds x in B . (n + k) )

proof

let B be SetSequence of X; :: thesis: ( x in Union (inferior_setsequence B) iff ex n being Nat st
for k being Nat holds x in B . (n + k) )
lim_inf B = Union (inferior_setsequence B) ;
hence ( x in Union (inferior_setsequence B) iff ex n being Nat st
for k being Nat holds x in B . (n + k) ) by KURATO_0:4; :: thesis: verum

end;

hence ( x in lim_inf S iff ex n being Nat st
for k being Nat holds x in S . (n + k) ) ; :: thesis: verum