for E being non empty finite set
for ASeq being SetSequence of E st ASeq is non-ascending holds
ex N being Nat st
for m being Nat st N <= m holds
ASeq . N = ASeq . m