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