theorem :: ORDERS_5:69

for A being RelStr
for B, C being Subset of A
for s being FinSequence of A st s is B -desc_ordering & C c= B holds
ex s2 being FinSequence of A st s2 is C -desc_ordering