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 )
hereby :: thesis: ( Rev s is B -desc_ordering implies 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;
assume A4: Rev s is B -desc_ordering ; :: thesis: s is B -asc_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