set V = { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ;
set Y = meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ;

A1: now :: thesis: for A being set st A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } holds
S c= A

let A be set ; :: thesis: ( A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } implies S c= A )
assume A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ; :: thesis: S c= A
then ex Z being Subset-Family of X st
( A = Z & S c= Z & Z is SigmaRing of X ) ;
hence S c= A ; :: thesis: verum

end;

for F being SetSequence of X st rng F c= bool X holds
Union F in bool X ;
then reconsider BX = bool X as SigmaRing of X by DefSigmaRing;
B1: BX in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ;
A3: meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } c= bool X by B1, SETFAM_1:def 1;

now :: thesis: for x, y being set st x in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } & y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } holds
x \ y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) }

let x, y be set ; :: thesis: ( x in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } & y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } implies x \ y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } )
assume C1: ( x in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } & y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ) ; :: thesis: x \ y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) }

now :: thesis: for A being set st A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } holds
x \ y in A

let A be set ; :: thesis: ( A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } implies x \ y in A )
assume C3: A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ; :: thesis: x \ y in A
then consider Z being Subset-Family of X such that
C2: ( A = Z & S c= Z & Z is SigmaRing of X ) ;
( x in A & y in A ) by C1, C3, SETFAM_1:def 1;
hence x \ y in A by C2, FINSUB_1:def 3; :: thesis: verum

end;

hence x \ y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } by B1, SETFAM_1:def 1; :: thesis: verum

end;

then A4: meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } is diff-closed ;

now :: thesis: for x, y being set st x in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } & y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } holds
x \/ y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) }

let x, y be set ; :: thesis: ( x in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } & y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } implies x \/ y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } )
assume F1: ( x in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } & y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ) ; :: thesis: x \/ y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) }

now :: thesis: for A being set st A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } holds
x \/ y in A

let A be set ; :: thesis: ( A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } implies x \/ y in A )
assume F2: A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ; :: thesis: x \/ y in A
then consider Z being Subset-Family of X such that
F3: ( A = Z & S c= Z & Z is SigmaRing of X ) ;
( x in A & y in A ) by F1, F2, SETFAM_1:def 1;
hence x \/ y in A by F3, FINSUB_1:def 1; :: thesis: verum

end;

hence x \/ y in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } by B1, SETFAM_1:def 1; :: thesis: verum

end;

then E1: meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } is cup-closed ;

A5: now :: thesis: for F being SetSequence of X st rng F c= meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } holds
Union F in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) }

let F be SetSequence of X; :: thesis: ( rng F c= meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } implies Union F in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } )
assume D1: rng F c= meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ; :: thesis: Union F in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) }

now :: thesis: for A being set st A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } holds
Union F in A

let A be set ; :: thesis: ( A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } implies Union F in A )
assume D2: A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ; :: thesis: Union F in A
then consider Z being Subset-Family of X such that
D3: ( A = Z & S c= Z & Z is SigmaRing of X ) ;
meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } c= A by D2, SETFAM_1:3;
then rng F c= A by D1;
hence Union F in A by D3, DefSigmaRing; :: thesis: verum

end;

hence Union F in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } by B1, SETFAM_1:def 1; :: thesis: verum

end;

now :: thesis: for A being set st A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } holds
{} in A

let A be set ; :: thesis: ( A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } implies {} in A )
assume A in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ; :: thesis: {} in A
then ex Z being Subset-Family of X st
( A = Z & S c= Z & Z is SigmaRing of X ) ;
hence {} in A by NE; :: thesis: verum

end;

then {} in meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } by B1, SETFAM_1:def 1;
then reconsider Y = meet { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } as SigmaRing of X by E1, A3, A4, A5, DefSigmaRing;
take Y ; :: thesis: ( S c= Y & ( for Z being set st S c= Z & Z is SigmaRing of X holds
Y c= Z ) )
for F being SetSequence of X st rng F c= bool X holds
Union F in bool X ;
then reconsider BX = bool X as SigmaRing of X by DefSigmaRing;
BX in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ;
hence S c= Y by A1, SETFAM_1:5; :: thesis: for Z being set st S c= Z & Z is SigmaRing of X holds
Y c= Z

hereby :: thesis: verum

let Z be set ; :: thesis: ( S c= Z & Z is SigmaRing of X implies Y c= Z )
assume ( S c= Z & Z is SigmaRing of X ) ; :: thesis: Y c= Z
then Z in { Z where Z is Subset-Family of X : ( S c= Z & Z is SigmaRing of X ) } ;
hence Y c= Z by SETFAM_1:3; :: thesis: verum

end;