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