let X be set ; :: thesis: for Si being SigmaField of X
for XSeq being SetSequence of Si holds rng XSeq c= Si
let Si be SigmaField of X; :: thesis: for XSeq being SetSequence of Si holds rng XSeq c= Si
let XSeq be SetSequence of Si; :: thesis: rng XSeq c= Si
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng XSeq or x in Si )
assume x in rng XSeq ; :: thesis: x in Si
then ex n being Nat st x = XSeq . n by SETLIM_1:4;
hence x in Si ; :: thesis: verum