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 ) } ;

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 ) }

Intersection BSeq in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) }

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

Y c= Z ) ) by A2, A1, SETFAM_1:5; :: thesis: verum

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

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

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

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
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 ) }

end;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

hence
E ` in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) }
by A2, SETFAM_1:def 1; :: thesis: verumE ` 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 A4, SETFAM_1:def 1;

hence E ` in Z by Def1; :: thesis: verum

end;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 A4, SETFAM_1:def 1;

hence E ` in Z by Def1; :: thesis: verum

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 ) }

end;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

hence
Intersection BSeq in meet { S where S is Subset-Family of Omega : ( X c= S & S is SigmaField of Omega ) }
by A2, SETFAM_1:def 1; :: thesis: verumIntersection 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

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 A8, Def6; :: thesis: verum

end;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

then A8:
rng BSeq c= Z
by NAT_1:52;let n be Nat; :: thesis: BSeq . n in Z

BSeq . n in rng BSeq by NAT_1:51;

hence BSeq . n in Z by A6, A7, SETFAM_1:def 1; :: thesis: verum

end;BSeq . n in rng BSeq by NAT_1:51;

hence BSeq . n in Z by A6, A7, SETFAM_1:def 1; :: thesis: verum

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 A8, Def6; :: thesis: verum

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

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 A2, A5, A3, Def1, Def6, SETFAM_1:3, SETFAM_1:def 1;{} 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;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

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

hence
( X c= Y & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
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 A9, A10;

hence Y c= Z by SETFAM_1:3; :: thesis: verum

end;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 A9, A10;

hence Y c= Z by SETFAM_1:3; :: thesis: verum

Y c= Z ) ) by A2, A1, SETFAM_1:5; :: thesis: verum