let f be FinSequence; :: thesis: Center f >= 1
((len f) div 2) + 1 >= 0 + 1 by XREAL_1:6;
hence Center f >= 1 by JORDAN1A:def 1; :: thesis: verum