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 A1: ( D is Dynkin_System of Omega & D is intersection_stable ) ; :: thesis: for x being finite set st x c= D holds
union x in D
let x be finite set ; :: thesis: ( x c= D implies union x in D )
assume A2: x c= D ; :: thesis: union x in D
defpred S₁[ set ] means union $1 in D;
A3: x is finite ;
A4: S₁[ {} ] by A1, Def7, ZFMISC_1:2;
A5: 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 A6: ( y in x & b c= x & union b in D ) ; :: thesis: S₁[b \/ {y}]
A7: union {y} = y by ZFMISC_1:31;
reconsider unionb = union b as Subset of Omega by A6;
y in D by A2, A6;
then reconsider y1 = y as Subset of Omega ;
unionb \/ y1 in D by A1, A2, A6, Th17;
hence S₁[b \/ {y}] by A7, ZFMISC_1:96; :: thesis: verum

end;

thus S₁[x] from FINSET_1:sch 2(A3, A4, A5); :: thesis: verum