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

proof

let n, m be Element of NAT ; :: thesis: ( n <= m implies (A1 (\) A) . m c= (A1 (\) A) . n )
assume n <= m ; :: thesis: (A1 (\) A) . m c= (A1 (\) A) . n
then A1 . m c= A1 . n by A1, PROB_1:def 4;
then (A1 . m) \ A c= (A1 . n) \ A by XBOOLE_1:33;
then (A1 (\) A) . m c= (A1 . n) \ A by Def8;
hence (A1 (\) A) . m c= (A1 (\) A) . n by Def8; :: thesis: verum

end;

hence A1 (\) A is non-ascending by PROB_1:def 4; :: thesis: verum