let X be set ; :: thesis: for S being semialgebra_of_sets of X holds Field_generated_by S = DisUnion S
let S be semialgebra_of_sets of X; :: thesis: Field_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;

now :: thesis: for A being set st A in R holds
X \ A in R

let A be set ; :: thesis: ( A in R implies X \ A in R )
assume C1: A in R ; :: thesis: X \ A in R
X in R by A0, Def1;
hence X \ A in R by C1, FINSUB_1:def 3; :: thesis: verum

end;

then K2: R is compl-closed by MEASURE1:def 1;
A10: R in { Z where Z is Field_Subset of X : S c= Z } by A0, K2;

now :: thesis: for x being object st x in R holds
x in Field_generated_by S

let x be object ; :: thesis: ( x in R implies x in Field_generated_by S )
assume x in R ; :: thesis: x in Field_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 Field_Subset of X : S c= Z } holds
x in Y

proof

let Y be set ; :: thesis: ( Y in { Z where Z is Field_Subset of X : S c= Z } implies x in Y )
assume Y in { Z where Z is Field_Subset of X : S c= Z } ; :: thesis: x in Y
then consider Z being Field_Subset of X such that
A11: ( Y = Z & S c= Z ) ;
defpred S₁[ Nat] means union (rng (F | $1)) in Z;
X1: S₁[ 0 ] by SETFAM_1:def 8, ZFMISC_1:2;
X2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume X3: S₁[k] ; :: thesis: S₁[k + 1]

per cases ( k + 1 <= len F or k + 1 > len F ) ;

suppose C4: k + 1 <= len F ; :: thesis: S₁[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 S₁[k + 1] by X3, C6, FINSUB_1:def 1; :: thesis: verum

end;

suppose k + 1 > len F ; :: thesis: S₁[k + 1]

then ( F | k = F & F | (k + 1) = F ) by FINSEQ_1:58, NAT_1:13;
hence S₁[k + 1] by X3; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(X1, X2);
then S₁[ len F] ;
hence x in Y by A8, A9, A11, FINSEQ_1:58; :: thesis: verum

end;

hence x in Field_generated_by S by A10, SETFAM_1:def 1; :: thesis: verum

end;

then R c= Field_generated_by S ;
hence Field_generated_by S = DisUnion S by A10, SETFAM_1:7; :: thesis: verum