for A being antisymmetric RelStr
for B being Subset of A
for s1, s2 being FinSequence of A st s1 is B -desc_ordering & s2 is B -desc_ordering holds
s1 = s2