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

for S being SetSequence of Si holds Intersection S c= lim_inf S

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

let S be SetSequence of Si; :: thesis: Intersection S c= lim_inf S

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

assume x in Intersection S ; :: thesis: x in lim_inf S

then for k being Nat holds x in S . (0 + k) by PROB_1:13;

hence x in lim_inf S by Th67; :: thesis: verum

for S being SetSequence of Si holds Intersection S c= lim_inf S

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

let S be SetSequence of Si; :: thesis: Intersection S c= lim_inf S

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

assume x in Intersection S ; :: thesis: x in lim_inf S

then for k being Nat holds x in S . (0 + k) by PROB_1:13;

hence x in lim_inf S by Th67; :: thesis: verum