theorem Th18: :: PROB_4:18

for X being set
for A1 being SetSequence of X st A1 is non-descending holds
for n being Nat holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n