for A being transitive connected RelStr
for B being finite Subset of A ex s being FinSequence of A st s is B -desc_ordering