theorem Th73: :: ORDERS_5:61

for A being RelStr
for s being FinSequence of A holds
( s is weakly-ascending iff Rev s is weakly-descending )