theorem :: ORDERS_5:62

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