theorem :: JORDAN1B:12

for f being FinSequence st len f >= 1 holds
Center f <= len f