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 )

( 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 A2:
Complement ASeq is non-ascending
; :: thesis: ASeq is non-descending
assume A1:
ASeq is non-descending
; :: thesis: Complement ASeq is non-ascending

end;now :: thesis: for n, m being Nat st n <= m holds

(Complement ASeq) . m c= (Complement ASeq) . n

hence
Complement ASeq is non-ascending
; :: thesis: verum(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;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

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

ASeq . n c= ASeq . m

hence
ASeq is non-descending
; :: thesis: verumASeq . 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;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