let X be set ; :: thesis: for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds P c= Ring_generated_by P
let P be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: P c= Ring_generated_by P
set Y = { Z where Z is non empty preBoolean Subset-Family of X : P c= Z } ;
A1: bool X in { Z where Z is non empty preBoolean Subset-Family of X : P c= Z } ;
for A being set st A in { Z where Z is non empty preBoolean Subset-Family of X : P c= Z } holds
P c= A
proof
let A be set ; :: thesis: ( A in { Z where Z is non empty preBoolean Subset-Family of X : P c= Z } implies P c= A )
assume A in { Z where Z is non empty preBoolean Subset-Family of X : P c= Z } ; :: thesis: P c= A
then ex Z being non empty preBoolean Subset-Family of X st
( A = Z & P c= Z ) ;
hence P c= A ; :: thesis: verum
end;
hence P c= Ring_generated_by P by A1, SETFAM_1:5; :: thesis: verum