let X, 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 Element of NAT st
for k being Element of 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 Element of NAT st
for k being Element of NAT holds x in S . (n + k) )
let S be SetSequence of Si; :: thesis: ( x in lim_inf S iff ex n being Element of NAT st
for k being Element of NAT holds x in S . (n + k) )
for B being SetSequence of X holds
( x in Union (inferior_setsequence B) iff ex n being Element of NAT st
for k being Element of 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 Element of NAT st
for k being Element of 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 Element of NAT st
for k being Element of NAT holds x in B . (n + k) ) by KURATO_2:7; :: thesis: verum

end;

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