let X, S be set ; :: thesis: ( S is SigmaRing of X & X in S implies S is SigmaField of X )
assume that
A1: S is SigmaRing of X and
A2: X in S ; :: thesis: S is SigmaField of X
reconsider S1 = S as non empty Subset-Family of X by A1;
A3: S1 is diff-closed by A1;

P1: now :: thesis: for A being Subset of X st A in S1 holds
A ` in S1

let A be Subset of X; :: thesis: ( A in S1 implies A ` in S1 )
assume A in S1 ; :: thesis: A ` in S1
then X \ A in S1 by A2, A3;
hence A ` in S1 by SUBSET_1:def 4; :: thesis: verum

end;

X c= X ;
then reconsider X1 = X as Subset of X ;

now :: thesis: for A being SetSequence of X st rng A c= S1 holds
Intersection A in S1

let A be SetSequence of X; :: thesis: ( rng A c= S1 implies Intersection A in S1 )
assume P2: rng A c= S1 ; :: thesis: Intersection A in S1

now :: thesis: for a being object st a in rng (Complement A) holds
a in S1

let a be object ; :: thesis: ( a in rng (Complement A) implies a in S1 )
assume a in rng (Complement A) ; :: thesis: a in S1
then consider n being Element of NAT such that
P3: a = (Complement A) . n by FUNCT_2:113;
a = (A . n) ` by P3, PROB_1:def 2;
then P4: a = X \ (A . n) by SUBSET_1:def 4;
A . n in rng A by FUNCT_2:4;
hence a in S1 by P4, P2, A1, A2, FINSUB_1:def 3; :: thesis: verum

end;

then rng (Complement A) c= S1 ;
then Union (Complement A) in S1 by A1, DefSigmaRing;
then X1 \ (Union (Complement A)) in S1 by A1, A2, FINSUB_1:def 3;
then (Union (Complement A)) ` in S1 by SUBSET_1:def 4;
hence Intersection A in S1 by PROB_1:def 3; :: thesis: verum

end;

hence S is SigmaField of X by P1, PROB_1:def 1, PROB_1:def 6; :: thesis: verum