let X be non empty set ; :: thesis: for S being semialgebra_of_sets of X holds sigma (Field_generated_by S) = sigma S
let S be semialgebra_of_sets of X; :: thesis: sigma (Field_generated_by S) = sigma S
A1: S c= Field_generated_by S by FieldGen1;
Field_generated_by S c= sigma (Field_generated_by S) by PROB_1:def 9;
then A2: S c= sigma (Field_generated_by S) by A1;
now :: thesis: for x being object st x in Field_generated_by S holds
x in sigma S
let x be object ; :: thesis: ( x in Field_generated_by S implies x in sigma S )
assume A3: x in Field_generated_by S ; :: thesis: x in sigma S
S c= sigma S by PROB_1:def 9;
then sigma S in { Z where Z is Field_Subset of X : S c= Z } ;
hence x in sigma S by A3, SETFAM_1:def 1; :: thesis: verum
end;
then Field_generated_by S c= sigma S ;
hence sigma (Field_generated_by S) = sigma S by A2, PROB_1:def 9; :: thesis: verum