let X be set ; :: thesis: for Si being SigmaField of X

for S being SetSequence of Si holds lim_sup S c= Union S

let Si be SigmaField of X; :: thesis: for S being SetSequence of Si holds lim_sup S c= Union S

let S be SetSequence of Si; :: thesis: lim_sup S c= Union S

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_sup S or x in Union S )

assume x in lim_sup S ; :: thesis: x in Union S

then ex k being Nat st x in S . (0 + k) by Th66;

hence x in Union S by PROB_1:12; :: thesis: verum

for S being SetSequence of Si holds lim_sup S c= Union S

let Si be SigmaField of X; :: thesis: for S being SetSequence of Si holds lim_sup S c= Union S

let S be SetSequence of Si; :: thesis: lim_sup S c= Union S

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_sup S or x in Union S )

assume x in lim_sup S ; :: thesis: x in Union S

then ex k being Nat st x in S . (0 + k) by Th66;

hence x in Union S by PROB_1:12; :: thesis: verum