let X be set ; :: thesis: for Si being SigmaField of X
for S being SetSequence of Si st S is non-descending holds
lim_inf S = Union S
let Si be SigmaField of X; :: thesis: for S being SetSequence of Si st S is non-descending holds
lim_inf S = Union S
let S be SetSequence of Si; :: thesis: ( S is non-descending implies lim_inf S = Union S )
A00: for B being SetSequence of X st B is non-descending holds
Union (inferior_setsequence B) = Union B

proof

let B be SetSequence of X; :: thesis: ( B is non-descending implies Union (inferior_setsequence B) = Union B )
lim_inf B = Union (inferior_setsequence B) ;
hence ( B is non-descending implies Union (inferior_setsequence B) = Union B ) by Th49; :: thesis: verum

end;

thus ( S is non-descending implies lim_inf S = Union S ) by A00; :: thesis: verum