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