let Omega be set ; :: thesis: for ASeq being SetSequence of Omega holds
( ASeq is non-descending iff Complement ASeq is non-ascending )
let ASeq be SetSequence of Omega; :: thesis: ( ASeq is non-descending iff Complement ASeq is non-ascending )
thus ( ASeq is non-descending implies Complement ASeq is non-ascending ) :: thesis: ( Complement ASeq is non-ascending implies ASeq is non-descending )

proof

assume A1: ASeq is non-descending ; :: thesis: Complement ASeq is non-ascending

now :: thesis: for n, m being Nat st n <= m holds
(Complement ASeq) . m c= (Complement ASeq) . n

let n, m be Nat; :: thesis: ( n <= m implies (Complement ASeq) . m c= (Complement ASeq) . n )
assume n <= m ; :: thesis: (Complement ASeq) . m c= (Complement ASeq) . n
then ASeq . n c= ASeq . m by A1;
then (ASeq . m) ` c= (ASeq . n) ` by SUBSET_1:12;
then (Complement ASeq) . m c= (ASeq . n) ` by PROB_1:def 2;
hence (Complement ASeq) . m c= (Complement ASeq) . n by PROB_1:def 2; :: thesis: verum

end;

hence Complement ASeq is non-ascending ; :: thesis: verum

end;

assume A2: Complement ASeq is non-ascending ; :: thesis: ASeq is non-descending

now :: thesis: for n, m being Nat st n <= m holds
ASeq . n c= ASeq . m

let n, m be Nat; :: thesis: ( n <= m implies ASeq . n c= ASeq . m )
assume n <= m ; :: thesis: ASeq . n c= ASeq . m
then (Complement ASeq) . m c= (Complement ASeq) . n by A2;
then (ASeq . m) ` c= (Complement ASeq) . n by PROB_1:def 2;
then (ASeq . m) ` c= (ASeq . n) ` by PROB_1:def 2;
hence ASeq . n c= ASeq . m by SUBSET_1:12; :: thesis: verum

end;

hence ASeq is non-descending ; :: thesis: verum