let A be RelStr ; :: thesis: for B being Subset of A

for s being FinSequence of A holds

( s is B -asc_ordering iff Rev s is B -desc_ordering )

let B be Subset of A; :: thesis: for s being FinSequence of A holds

( s is B -asc_ordering iff Rev s is B -desc_ordering )

let s be FinSequence of A; :: thesis: ( s is B -asc_ordering iff Rev s is B -desc_ordering )

then A5: s is weakly-ascending by Th73;

A6: rng s = B by A4, FINSEQ_5:57;

Rev (Rev s) is one-to-one by A4;

hence s is B -asc_ordering by A5, A6; :: thesis: verum

for s being FinSequence of A holds

( s is B -asc_ordering iff Rev s is B -desc_ordering )

let B be Subset of A; :: thesis: for s being FinSequence of A holds

( s is B -asc_ordering iff Rev s is B -desc_ordering )

let s be FinSequence of A; :: thesis: ( s is B -asc_ordering iff Rev s is B -desc_ordering )

hereby :: thesis: ( Rev s is B -desc_ordering implies s is B -asc_ordering )

assume A4:
Rev s is B -desc_ordering
; :: thesis: s is B -asc_ordering assume A1:
s is B -asc_ordering
; :: thesis: Rev s is B -desc_ordering

then A2: Rev s is weakly-descending by Th73;

rng (Rev s) = B by A1, FINSEQ_5:57;

hence Rev s is B -desc_ordering by A2, A1; :: thesis: verum

end;then A2: Rev s is weakly-descending by Th73;

rng (Rev s) = B by A1, FINSEQ_5:57;

hence Rev s is B -desc_ordering by A2, A1; :: thesis: verum

then A5: s is weakly-ascending by Th73;

A6: rng s = B by A4, FINSEQ_5:57;

Rev (Rev s) is one-to-one by A4;

hence s is B -asc_ordering by A5, A6; :: thesis: verum