let X be set ; :: thesis: for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds Ring_generated_by S = DisUnion S
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: Ring_generated_by S = DisUnion S
set R = DisUnion S;
reconsider R = DisUnion S as non empty Subset-Family of X ;
A0: S c= R by lemma100;
A1: R is cap-closed by lemma101;
A2: now :: thesis: for A, B being set st A in R & B in R holds
B \ A in R
let A, B be set ; :: thesis: ( A in R & B in R implies B \ A in R )
assume A3: ( A in R & B in R ) ; :: thesis: B \ A in R
then ( A <> {} implies B \ A in R ) by lemma105;
hence B \ A in R by A3; :: thesis: verum
end;
then A4: R is diff-closed ;
now :: thesis: for A, B being set st A in R & B in R holds
A \/ B in R
let A, B be set ; :: thesis: ( A in R & B in R implies A \/ B in R )
assume ( A in R & B in R ) ; :: thesis: A \/ B in R
then A5: ( A \ B in R & B \ A in R & A /\ B in R ) by A2, A1;
(A \ B) \/ (B \ A) in R by A5, lemma102, XBOOLE_1:82;
then A6: A \+\ B in R by XBOOLE_0:def 6;
(A \+\ B) \/ (A /\ B) in R by A5, A6, lemma102, XBOOLE_1:103;
hence A \/ B in R by XBOOLE_1:93; :: thesis: verum
end;
then R is cup-closed ;
then reconsider R = R as non empty preBoolean Subset-Family of X by A4;
A10: R in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } by A0;
now :: thesis: for x being object st x in R holds
x in Ring_generated_by S
let x be object ; :: thesis: ( x in R implies x in Ring_generated_by S )
assume x in R ; :: thesis: x in Ring_generated_by S
then consider A being Subset of X such that
A8: ( x = A & ex F being disjoint_valued FinSequence of S st A = Union F ) ;
consider F being disjoint_valued FinSequence of S such that
A9: A = Union F by A8;
for Y being set st Y in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } holds
x in Y
proof
let Y be set ; :: thesis: ( Y in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } implies x in Y )
assume Y in { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ; :: thesis: x in Y
then consider Z being non empty preBoolean Subset-Family of X such that
A11: ( Y = Z & S c= Z ) ;
defpred S1[ Nat] means union (rng (F | $1)) in Z;
X1: S1[ 0 ] by SETFAM_1:def 8, ZFMISC_1:2;
X2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume X3: S1[k] ; :: thesis: S1[k + 1]
per cases ( k + 1 <= len F or k + 1 > len F ) ;
suppose C4: k + 1 <= len F ; :: thesis: S1[k + 1]
F | k = (F | (k + 1)) | k by NAT_1:11, FINSEQ_1:82;
then F | (k + 1) = (F | k) ^ <*((F | (k + 1)) . (k + 1))*> by C4, FINSEQ_1:59, FINSEQ_3:55;
then rng (F | (k + 1)) = (rng (F | k)) \/ (rng <*((F | (k + 1)) . (k + 1))*>) by FINSEQ_1:31
.= (rng (F | k)) \/ {((F | (k + 1)) . (k + 1))} by FINSEQ_1:38
.= (rng (F | k)) \/ {(F . (k + 1))} by FINSEQ_3:112 ;
then C6: union (rng (F | (k + 1))) = (union (rng (F | k))) \/ (union {(F . (k + 1))}) by ZFMISC_1:78
.= (union (rng (F | k))) \/ (F . (k + 1)) ;
k + 1 in dom F by C4, NAT_1:11, FINSEQ_3:25;
then ( F . (k + 1) in rng F & rng F c= S ) by FUNCT_1:3;
then F . (k + 1) in Z by A11;
hence S1[k + 1] by X3, C6, FINSUB_1:def 1; :: thesis: verum
end;
suppose k + 1 > len F ; :: thesis: S1[k + 1]
then ( F | k = F & F | (k + 1) = F ) by FINSEQ_1:58, NAT_1:13;
hence S1[k + 1] by X3; :: thesis: verum
end;
end;
end;
for k being Nat holds S1[k] from NAT_1:sch 2(X1, X2);
 then S1[ len F] ;
hence x in Y by A8, A9, A11, FINSEQ_1:58; :: thesis: verum
end;
hence x in Ring_generated_by S by A10, SETFAM_1:def 1; :: thesis: verum
end;
then R c= Ring_generated_by S ;
hence Ring_generated_by S = DisUnion S by A10, SETFAM_1:7; :: thesis: verum