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 )

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

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

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

hence
Complement ASeq is non-descending
; :: thesis: verum(Complement ASeq) . n c= (Complement ASeq) . m

let n, m be 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;

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;assume n <= m ; :: thesis: (Complement ASeq) . n c= (Complement ASeq) . m

then ASeq . m c= ASeq . n by A1;

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

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

ASeq . m c= ASeq . n

hence
ASeq is non-ascending
; :: thesis: verumASeq . m c= ASeq . n

let n, m be 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;

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;assume n <= m ; :: thesis: ASeq . m c= ASeq . n

then (Complement ASeq) . n c= (Complement ASeq) . m by A2;

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