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)

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

hence
lim_inf S c= lim_sup S
; :: thesis: verum
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;( 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