per cases ( D is empty or not D is empty ) ;

suppose A1: D is empty ; :: thesis: UniCl D is sigma-additive

now :: thesis: for M being N_Sub_set_fam of X st M c= UniCl D holds
union M in UniCl D

let M be N_Sub_set_fam of X; :: thesis: ( M c= UniCl D implies union b₁ in UniCl D )
assume M c= UniCl D ; :: thesis: union b₁ in UniCl D
then M c= {{}} by A1, YELLOW_9:16;

per cases then ( M = {} or M = {{}} ) by ZFMISC_1:33;

suppose M = {} ; :: thesis: union b₁ in UniCl D

hence union M in UniCl D ; :: thesis: verum

end;

suppose A2: M = {{}} ; :: thesis: union b₁ in UniCl D

{} c= D ;
then reconsider P = {} as Subset of D ;
union P = union M by A2, ZFMISC_1:2;
then union M in { (union P) where P is Subset of D : verum } ;
hence union M in UniCl D by Th14; :: thesis: verum

end;

end;

end;

hence UniCl D is sigma-additive ; :: thesis: verum

end;

suppose A3: not D is empty ; :: thesis: UniCl D is sigma-additive

now :: thesis: for M being N_Sub_set_fam of X st M c= UniCl D holds
union M in UniCl D

let M be N_Sub_set_fam of X; :: thesis: ( M c= UniCl D implies union M in UniCl D )
assume A4: M c= UniCl D ; :: thesis: union M in UniCl D
{ p where p is Element of D : p c= union M } c= D

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { p where p is Element of D : p c= union M } or t in D )
assume t in { p where p is Element of D : p c= union M } ; :: thesis: t in D
then ex p being Element of D st
( t = p & p c= union M ) ;
hence t in D by A3; :: thesis: verum

end;

then reconsider P = { p where p is Element of D : p c= union M } as Subset of D ;
union M = union P

proof

thus union M c= union P :: according to XBOOLE_0:def 10 :: thesis: union P c= union M

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in union M or t in union P )
assume t in union M ; :: thesis: t in union P
then consider y being set such that
A6: t in y and
A7: y in M by TARSKI:def 4;
y in UniCl D by A7, A4;
then y in { (union Q) where Q is Subset of D : verum } by Th14;
then consider Q being Subset of D such that
A8: y = union Q ;
consider z being set such that
A9: t in z and
A10: z in Q by A6, A8, TARSKI:def 4;
reconsider z = z as Element of D by A10;
A11: z c= y by A8, A10, ZFMISC_1:74;
y c= union M by A7, ZFMISC_1:74;
then z c= union M by A11;
then z in P ;
hence t in union P by A9, TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union P or x in union M )
assume x in union P ; :: thesis: x in union M
then consider y being set such that
A12: x in y and
A13: y in P by TARSKI:def 4;
ex p being Element of D st
( y = p & p c= union M ) by A13;
hence x in union M by A12; :: thesis: verum

end;

then union M in { (union P) where P is Subset of D : verum } ;
hence union M in UniCl D by Th14; :: thesis: verum

end;

hence UniCl D is sigma-additive ; :: thesis: verum

end;

end;