theorem Th82: :: ORDERS_5:70

for A being RelStr
for B being Subset of A
for s being FinSequence of A
for x being Element of A st B = {x} & s = <*x*> holds
( s is B -asc_ordering & s is B -desc_ordering )