let X be set ; :: thesis: for Si being SigmaField of X
for S being SetSequence of Si holds lim_inf S c= lim_sup S
let Si be SigmaField of X; :: thesis: for S being SetSequence of Si holds lim_inf S c= lim_sup S
let S be SetSequence of Si; :: thesis: lim_inf S c= lim_sup S
for B being SetSequence of X holds Union (inferior_setsequence B) c= Intersection (superior_setsequence B)

proof

let B be SetSequence of X; :: thesis: Union (inferior_setsequence B) c= Intersection (superior_setsequence B)
( lim_inf B = Union (inferior_setsequence B) & lim_sup B = Intersection (superior_setsequence B) ) ;
hence Union (inferior_setsequence B) c= Intersection (superior_setsequence B) by KURATO_0:6; :: thesis: verum

end;

hence lim_inf S c= lim_sup S ; :: thesis: verum