let X be set ; :: thesis: for A1 being SetSequence of X holds Partial_Union A1 is non-descending
let A1 be SetSequence of X; :: thesis: Partial_Union A1 is non-descending

now :: thesis: for n being Nat holds (Partial_Union A1) . n c= (Partial_Union A1) . (n + 1)

let n be Nat; :: thesis: (Partial_Union A1) . n c= (Partial_Union A1) . (n + 1)
(Partial_Union A1) . (n + 1) = ((Partial_Union A1) . n) \/ (A1 . (n + 1)) by Def2;
hence (Partial_Union A1) . n c= (Partial_Union A1) . (n + 1) by XBOOLE_1:7; :: thesis: verum

end;

hence Partial_Union A1 is non-descending by PROB_2:7; :: thesis: verum