let X be set ; :: thesis: for F being Field_Subset of X ex S being semialgebra_of_sets of X st
( F = S & F = Field_generated_by S )
let F be Field_Subset of X; :: thesis: ex S being semialgebra_of_sets of X st
( F = S & F = Field_generated_by S )
reconsider S = F as semialgebra_of_sets of X by SRINGS_3:20;
take S ; :: thesis: ( F = S & F = Field_generated_by S )
now :: thesis: for x being object st x in Field_generated_by S holds
x in S
let x be object ; :: thesis: ( x in Field_generated_by S implies x in S )
assume x in Field_generated_by S ; :: thesis: x in S
then A2: x in meet { Z where Z is Field_Subset of X : S c= Z } by SRINGS_3:def 7;
F in { Z where Z is Field_Subset of X : S c= Z } ;
hence x in S by A2, SETFAM_1:def 1; :: thesis: verum
end;
then Field_generated_by S c= S ;
hence ( F = S & F = Field_generated_by S ) by SRINGS_3:21; :: thesis: verum