for X being set
for S being non empty set holds
( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Intersection A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) ) by Def1, Def6;