let Omega be non empty set ; :: thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for x being finite set st x c= D holds
union x in D
let D be non empty Subset-Family of Omega; :: thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies for x being finite set st x c= D holds
union x in D )
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; :: thesis: for x being finite set st x c= D holds
union x in D
defpred S₁[ set ] means union $1 in D;
let x be finite set ; :: thesis: ( x c= D implies union x in D )
assume A3: x c= D ; :: thesis: union x in D
A4: for y, b being set st y in x & b c= x & S₁[b] holds
S₁[b \/ {y}]

proof

let y, b be set ; :: thesis: ( y in x & b c= x & S₁[b] implies S₁[b \/ {y}] )
assume that
A5: y in x and
b c= x and
A6: union b in D ; :: thesis: S₁[b \/ {y}]
y in D by A3, A5;
then reconsider y1 = y as Subset of Omega ;
reconsider unionb = union b as Subset of Omega by A6;
( union {y} = y & unionb \/ y1 in D ) by A1, A2, A3, A5, A6, Th13, ZFMISC_1:25;
hence S₁[b \/ {y}] by ZFMISC_1:78; :: thesis: verum

end;

A7: x is finite ;
A8: S₁[ {} ] by A1, Def5, ZFMISC_1:2;
thus S₁[x] from FINSET_1:sch 2(A7, A8, A4); :: thesis: verum