let X be set ; :: thesis: for S being semialgebra_of_sets of X ex Y being Field_Subset of X st Y = meet { Z where Z is Field_Subset of X : S c= Z }
let S be semialgebra_of_sets of X; :: thesis: ex Y being Field_Subset of X st Y = meet { Z where Z is Field_Subset of X : S c= Z }
set V = { Z where Z is Field_Subset of X : S c= Z } ;
A1: bool X in { Z where Z is Field_Subset of X : S c= Z } ;
then reconsider Y = meet { Z where Z is Field_Subset of X : S c= Z } as Subset-Family of X by SETFAM_1:3;
now :: thesis: for Z being set st Z in { Z where Z is Field_Subset of X : S c= Z } holds
{} in Z
let Z be set ; :: thesis: ( Z in { Z where Z is Field_Subset of X : S c= Z } implies {} in Z )
assume Z in { Z where Z is Field_Subset of X : S c= Z } ; :: thesis: {} in Z
then ex S1 being Field_Subset of X st
( Z = S1 & S c= S1 ) ;
hence {} in Z by SETFAM_1:def 8; :: thesis: verum
end;
then A2: not Y is empty by A1, SETFAM_1:def 1;
now :: thesis: for A, B being set st A in Y & B in Y holds
A \/ B in Y
let A, B be set ; :: thesis: ( A in Y & B in Y implies A \/ B in Y )
assume B1: ( A in Y & B in Y ) ; :: thesis: A \/ B in Y
for Z being set st Z in { Z where Z is Field_Subset of X : S c= Z } holds
A \/ B in Z
proof
let Z be set ; :: thesis: ( Z in { Z where Z is Field_Subset of X : S c= Z } implies A \/ B in Z )
assume B2: Z in { Z where Z is Field_Subset of X : S c= Z } ; :: thesis: A \/ B in Z
then consider Z1 being Field_Subset of X such that
B3: ( Z = Z1 & S c= Z1 ) ;
( A in Z1 & B in Z1 ) by B1, B2, B3, SETFAM_1:def 1;
hence A \/ B in Z by B3, FINSUB_1:def 1; :: thesis: verum
end;
hence A \/ B in Y by A1, SETFAM_1:def 1; :: thesis: verum
end;
then B4: Y is cup-closed ;
now :: thesis: for A being set st A in Y holds
X \ A in Y
let A be set ; :: thesis: ( A in Y implies X \ A in Y )
assume C1: A in Y ; :: thesis: X \ A in Y
for Z being set st Z in { Z where Z is Field_Subset of X : S c= Z } holds
X \ A in Z
proof
let Z be set ; :: thesis: ( Z in { Z where Z is Field_Subset of X : S c= Z } implies X \ A in Z )
assume C2: Z in { Z where Z is Field_Subset of X : S c= Z } ; :: thesis: X \ A in Z
then consider Z1 being Field_Subset of X such that
C3: ( Z = Z1 & S c= Z1 ) ;
( A in Z1 & X in Z1 ) by Def1, C1, C2, C3, SETFAM_1:def 1;
hence X \ A in Z by C3, FINSUB_1:def 3; :: thesis: verum
end;
hence X \ A in Y by A1, SETFAM_1:def 1; :: thesis: verum
end;
then Y is compl-closed by MEASURE1:def 1;
hence ex Y being Field_Subset of X st Y = meet { Z where Z is Field_Subset of X : S c= Z } by A2, B4; :: thesis: verum