for X being set
for G being non empty finite FinSequenceSet of X ex A being FinSequence st
( A in G & ( for B being FinSequence st B in G holds
len B <= len A ) )