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) )

for k being Nat holds x in S . (n + k) ) ; :: thesis: verum

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

hence
( x in lim_inf S iff ex n being Nat st
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;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

for k being Nat holds x in S . (n + k) ) ; :: thesis: verum