let X be set ; :: thesis: for Si being SigmaField of X
for S being SetSequence of holds lim_sup S c= Union S
let Si be SigmaField of X; :: thesis: for S being SetSequence of holds lim_sup S c= Union S
let S be SetSequence of ; :: thesis: lim_sup S c= Union S
let x be set ; :: 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 consider k being Element of NAT such that
B: x in S . (0 + k) by Th55;
thus x in Union S by B, PROB_1:25; :: thesis: verum