let X be set ; :: thesis: for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds sigmaring (Ring_generated_by S) = sigmaring S
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: sigmaring (Ring_generated_by S) = sigmaring S
A1: S c= Ring_generated_by S by RingGen1;
Ring_generated_by S c= sigmaring (Ring_generated_by S) by Defsigmaring;
then A2: S c= sigmaring (Ring_generated_by S) by A1;
now :: thesis: for x being object st x in Ring_generated_by S holds
x in sigmaring S
let x be object ; :: thesis: ( x in Ring_generated_by S implies x in sigmaring S )
assume A3: x in Ring_generated_by S ; :: thesis: x in sigmaring S
S c= sigmaring S by Defsigmaring;
then sigmaring S in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ;
hence x in sigmaring S by A3, SETFAM_1:def 1; :: thesis: verum
end;
then Ring_generated_by S c= sigmaring S ;
hence sigmaring (Ring_generated_by S) = sigmaring S by A2, Defsigmaring; :: thesis: verum