let X be set ; :: thesis: for P being semialgebra_of_sets of X holds P c= Field_generated_by P
let P be semialgebra_of_sets of X; :: thesis: P c= Field_generated_by P
set Y = { Z where Z is Field_Subset of X : P c= Z } ;
A1: bool X in { Z where Z is Field_Subset of X : P c= Z } ;
for A being set st A in { Z where Z is Field_Subset of X : P c= Z } holds
P c= A

proof

let A be set ; :: thesis: ( A in { Z where Z is Field_Subset of X : P c= Z } implies P c= A )
assume A in { Z where Z is Field_Subset of X : P c= Z } ; :: thesis: P c= A
then ex Z being Field_Subset of X st
( A = Z & P c= Z ) ;
hence P c= A ; :: thesis: verum

end;

hence P c= Field_generated_by P by A1, SETFAM_1:5; :: thesis: verum