let Omega be non empty set ; :: thesis:
let X be Subset-Family of Omega; :: thesis:
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: bool Omega in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) }

proof

bool Omega c= bool Omega ;
then reconsider X1 = bool Omega as Subset-Family of Omega ;
X1 is SigmaField of Omega by Th76;
hence bool Omega in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; :: thesis:

end;

A2: now

let Z be set ; :: thesis:
assume Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; :: thesis:
then ex S being Subset-Family of Omega st
( Z = S & X c= S & S is SigmaField of Omega ) ;
hence {} in Z by Th10; :: thesis:

end;

A3: 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:
assume A4: rng BSeq c= meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; :: thesis:

now

let Z be set ; :: thesis:
assume A5: Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; :: thesis:
then A6: ex S being Subset-Family of Omega st
( Z = S & X c= S & S is SigmaField of Omega ) ;

now

let n be Nat; :: thesis:
BSeq . n in rng BSeq by NAT_1:52;
hence BSeq . n in Z by A5, A4, SETFAM_1:def 1; :: thesis:

end;

then rng BSeq c= Z by NAT_1:53;
hence Intersection BSeq in Z by A6, Def8; :: thesis:

end;

hence Intersection BSeq in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } by A1, SETFAM_1:def 1; :: thesis:

end;

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:
assume A7: E in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; :: thesis:

now

let Z be set ; :: thesis:
assume A8: Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } ; :: thesis:
then A9: E in Z by A7, SETFAM_1:def 1;
ex S being Subset-Family of Omega st
( Z = S & X c= S & S is SigmaField of Omega ) by A8;
hence E ` in Z by A9, Def1; :: thesis:

end;

hence E ` in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } by A1, SETFAM_1:def 1; :: thesis:

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 A1, A2, A3, Def1, Def8, SETFAM_1:4, SETFAM_1:def 1;
take Y ; :: thesis:

A10: now

end;

for Z being set st X c= Z & Z is SigmaField of Omega holds
Y c= Z

proof

let Z be set ; :: thesis:
assume A11: ( X c= Z & Z is SigmaField of Omega ) ; :: thesis:
then reconsider Z = Z as Subset-Family of Omega ;
Z in { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) } by A11;
hence Y c= Z by SETFAM_1:4; :: thesis:

end;

hence ( X c= Y & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
Y c= Z ) ) by A1, A10, SETFAM_1:6; :: thesis: