let f be FinSequence; :: thesis: ( len f >= 1 implies Center f <= len f )
assume len f >= 1 ; :: thesis: Center f <= len f
then 0 + (len f) < (len f) + (len f) by XREAL_1:6;
then (len f) + 1 <= 2 * (len f) by NAT_1:13;
then (((len f) + 1) + 1) div 2 <= len f by NAT_2:25;
then ((len f) + (1 + 1)) div 2 <= len f ;
then ((len f) div 2) + 1 <= len f by NAT_2:14;
hence Center f <= len f by JORDAN1A:def 1; :: thesis: verum