let X be set ; :: thesis: for S being SigmaRing of X holds S is sigma-multiplicative
let S be SigmaRing of X; :: thesis: S is sigma-multiplicative

now :: thesis: for F being SetSequence of X st rng F c= S holds
Intersection F in S

let F be SetSequence of X; :: thesis: ( rng F c= S implies Intersection F in S )
assume A1: rng F c= S ; :: thesis: Intersection F in S
then A2: Union F in S by DefSigmaRing;
reconsider UF = Union F as Subset of X ;

now :: thesis: for x being object st x in Intersection F holds
x in UF \ (Union (UF (\) F))

let x be object ; :: thesis: ( x in Intersection F implies x in UF \ (Union (UF (\) F)) )
assume BB: x in Intersection F ; :: thesis: x in UF \ (Union (UF (\) F))
B0: Intersection F c= UF by SETLIM_1:9;

now :: thesis: not x in Union (UF (\) F)

assume x in Union (UF (\) F) ; :: thesis: contradiction
then consider m being Nat such that
B1: x in (UF (\) F) . m by PROB_1:12;
x in UF \ (F . m) by B1, SETLIM_2:def 7;
then not x in F . m by XBOOLE_0:def 5;
hence contradiction by BB, PROB_1:13; :: thesis: verum

end;

hence x in UF \ (Union (UF (\) F)) by BB, B0, XBOOLE_0:def 5; :: thesis: verum

end;

then B3: Intersection F c= UF \ (Union (UF (\) F)) ;

now :: thesis: for x being object st x in UF \ (Union (UF (\) F)) holds
x in Intersection F

let x be object ; :: thesis: ( x in UF \ (Union (UF (\) F)) implies x in Intersection F )
assume x in UF \ (Union (UF (\) F)) ; :: thesis: x in Intersection F
then C3: ( x in UF & not x in Union (UF (\) F) ) by XBOOLE_0:def 5;

hereby :: thesis: verum

assume not x in Intersection F ; :: thesis: contradiction
then consider n being Nat such that
C2: not x in F . n by PROB_1:13;
x in UF \ (F . n) by C3, C2, XBOOLE_0:def 5;
then x in (UF (\) F) . n by SETLIM_2:def 7;
hence contradiction by C3, PROB_1:12; :: thesis: verum

end;

end;

then UF \ (Union (UF (\) F)) c= Intersection F ;
then B5: Intersection F = (Union F) \ (Union (UF (\) F)) by B3;

now :: thesis: for x being object st x in rng (UF (\) F) holds
x in S

let x be object ; :: thesis: ( x in rng (UF (\) F) implies x in S )
assume x in rng (UF (\) F) ; :: thesis: x in S
then consider n being Element of NAT such that
D1: x = (UF (\) F) . n by FUNCT_2:113;
D2: x = UF \ (F . n) by D1, SETLIM_2:def 7;
F . n in rng F by FUNCT_2:112;
hence x in S by A1, D2, A2, FINSUB_1:def 3; :: thesis: verum

end;

then rng (UF (\) F) c= S ;
then Union (UF (\) F) in S by DefSigmaRing;
hence Intersection F in S by A2, B5, FINSUB_1:def 3; :: thesis: verum

end;

hence S is sigma-multiplicative by PROB_1:def 6; :: thesis: verum