set V = { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ;
set Y = meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ;
A1: now :: thesis: for Z being set st Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } holds
X c= Z
let Z be set ; :: thesis: ( Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } implies X c= Z )
assume Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; :: thesis: X c= Z
then ex S being Subset-Family of Omega st
( Z = S & X c= S & S is SigmaField of Omega ) ;
hence X c= Z ; :: thesis: verum
end;
A2: bool Omega in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ;
A3: for E being Subset of Omega st E in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } holds
E ` in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) }
proof
let E be Subset of Omega; :: thesis: ( E in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } implies E ` in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } )
assume A4: E in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; :: thesis: E ` in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) }
now :: thesis: for Z being set st Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } holds
E ` in Z
let Z be set ; :: thesis: ( Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } implies E ` in Z )
assume Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; :: thesis: E ` in Z
then ( E in Z & ex S being Subset-Family of Omega st
( Z = S & X c= S & S is SigmaField of Omega ) ) by ;
hence E ` in Z by Def1; :: thesis: verum
end;
hence E ` in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } by ; :: thesis: verum
end;
A5: for BSeq being SetSequence of Omega st rng BSeq c= meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } holds
Intersection BSeq in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) }
proof
let BSeq be SetSequence of Omega; :: thesis: ( rng BSeq c= meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } implies Intersection BSeq in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } )
assume A6: rng BSeq c= meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; :: thesis: Intersection BSeq in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) }
now :: thesis: for Z being set st Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } holds
Intersection BSeq in Z
let Z be set ; :: thesis: ( Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } implies Intersection BSeq in Z )
assume A7: Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; :: thesis: Intersection BSeq in Z
now :: thesis: for n being Nat holds BSeq . n in Z
let n be Nat; :: thesis: BSeq . n in Z
BSeq . n in rng BSeq by NAT_1:51;
hence BSeq . n in Z by ; :: thesis: verum
end;
then A8: rng BSeq c= Z by NAT_1:52;
ex S being Subset-Family of Omega st
( Z = S & X c= S & S is SigmaField of Omega ) by A7;
hence Intersection BSeq in Z by ; :: thesis: verum
end;
hence Intersection BSeq in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } by ; :: thesis: verum
end;
now :: thesis: for Z being set st Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } holds
{} in Z
let Z be set ; :: thesis: ( Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } implies {} in Z )
assume Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; :: thesis: {} in Z
then ex S being Subset-Family of Omega st
( Z = S & X c= S & S is SigmaField of Omega ) ;
hence {} in Z by Th4; :: thesis: verum
end;
then reconsider Y = meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } as SigmaField of Omega by ;
take Y ; :: thesis: ( X c= Y & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
Y c= Z ) )

for Z being set st X c= Z & Z is SigmaField of Omega holds
Y c= Z
proof
let Z be set ; :: thesis: ( X c= Z & Z is SigmaField of Omega implies Y c= Z )
assume that
A9: X c= Z and
A10: Z is SigmaField of Omega ; :: thesis: Y c= Z
reconsider Z = Z as Subset-Family of Omega by A10;
Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } by ;
hence Y c= Z by SETFAM_1:3; :: thesis: verum
end;
hence ( X c= Y & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
Y c= Z ) ) by ; :: thesis: verum