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

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

let n be Nat; :: thesis: (Partial_Intersection A1) . (n + 1) c= (Partial_Intersection A1) . n
(Partial_Intersection A1) . (n + 1) = ((Partial_Intersection A1) . n) /\ (A1 . (n + 1)) by Def1;
hence (Partial_Intersection A1) . (n + 1) c= (Partial_Intersection A1) . n by XBOOLE_1:17; :: thesis: verum

end;

hence Partial_Intersection A1 is non-ascending by PROB_2:6; :: thesis: verum