let X be set ; :: thesis: 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
let A1 be SetSequence of X; :: thesis: ( A1 is non-descending implies for n being Nat holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n )
assume A1: A1 is non-descending ; :: thesis: for n being Nat holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n
let n be Nat; :: thesis: (Partial_Diff_Union A1) . (n + 1) misses A1 . n
(Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) by A1, Th16;
hence (Partial_Diff_Union A1) . (n + 1) misses A1 . n by XBOOLE_1:79; :: thesis: verum