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

let y, b be set ; :: thesis:
assume that
A5: y in x and
b c= x and
A6: union b in D ; :: thesis:
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:

end;