theorem Th79: :: ORDERS_5:67

for A being LinearOrder
for B being finite Subset of A
for s being FinSequence of A holds
( s is B -asc_ordering iff s = SgmX ( the InternalRel of A,B) )