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

proof

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

now

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

end;

hence Complement ASeq is non-descending by PROB_1:def 5; :: thesis: verum

end;

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

now

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

end;

hence ASeq is non-ascending by PROB_1:def 4; :: thesis: verum