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-ascending
let A be Subset of X; :: thesis: for A1 being SetSequence of X st A1 is non-descending holds
A (\) A1 is non-ascending
let A1 be SetSequence of X; :: thesis: ( A1 is non-descending implies A (\) A1 is non-ascending )
assume A1: A1 is non-descending ; :: thesis: A (\) A1 is non-ascending
for n, m being Nat st n <= m holds
(A (\) A1) . m c= (A (\) A1) . n
proof
let n, m be Nat; :: thesis: ( n <= m implies (A (\) A1) . m c= (A (\) A1) . n )
assume n <= m ; :: thesis: (A (\) A1) . m c= (A (\) A1) . n
then A1 . n c= A1 . m by A1, PROB_1:def 5;
then A \ (A1 . m) c= A \ (A1 . n) by XBOOLE_1:34;
then (A (\) A1) . m c= A \ (A1 . n) by Def7;
hence (A (\) A1) . m c= (A (\) A1) . n by Def7; :: thesis: verum
end;
hence A (\) A1 is non-ascending by PROB_1:def 4; :: thesis: verum