for A being RelStr
for B being Subset of A
for s being FinSequence of A st ( s is B -asc_ordering or s is B -desc_ordering ) holds
B is finite ;