let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is non-descending holds
A (/\) A1 is non-descending
let A be Subset of X; :: thesis: for A1 being SetSequence of X st A1 is non-descending holds
A (/\) A1 is non-descending
let A1 be SetSequence of X; :: thesis: ( A1 is non-descending implies A (/\) A1 is non-descending )
assume A1: A1 is non-descending ; :: thesis: A (/\) A1 is non-descending
for n, m being Nat st n <= m holds
(A (/\) A1) . n c= (A (/\) A1) . m

proof

let n, m be Nat; :: thesis: ( n <= m implies (A (/\) A1) . n c= (A (/\) A1) . m )
assume n <= m ; :: thesis: (A (/\) A1) . n c= (A (/\) A1) . m
then A1 . n c= A1 . m by A1, PROB_1:def 5;
then A /\ (A1 . n) c= A /\ (A1 . m) by XBOOLE_1:27;
then (A (/\) A1) . n c= A /\ (A1 . m) by Def5;
hence (A (/\) A1) . n c= (A (/\) A1) . m by Def5; :: thesis: verum

end;

hence A (/\) A1 is non-descending by PROB_1:def 5; :: thesis: verum