let p be XFinSequence; :: thesis: for k1, k2 being Nat st k1 > k2 holds
mid (p,k1,k2) = {}
let k1, k2 be Nat; :: thesis: ( k1 > k2 implies mid (p,k1,k2) = {} )
set k21 = k2;
A1: len (p | k2) <= k2 by AFINSQ_1:55;
assume A2: k1 > k2 ; :: thesis: mid (p,k1,k2) = {}
then k1 >= 0 + 1 by NAT_1:13;
then A3: k1 -' 1 = k1 - 1 by XREAL_1:233;
k1 >= k2 + 1 by A2, NAT_1:13;
then k1 - 1 >= (k2 + 1) - 1 by XREAL_1:9;
hence mid (p,k1,k2) = {} by A3, A1, Th6, XXREAL_0:2; :: thesis: verum