let f be XFinSequence; :: thesis: for k1, k2 being Nat st k1 > k2 holds
mid f,k1,k2 = {}
let k1, k2 be Nat; :: thesis: ( k1 > k2 implies mid f,k1,k2 = {} )
assume A6: k1 > k2 ; :: thesis: mid f,k1,k2 = {}
reconsider k11 = k1, k21 = k2 as Element of NAT by ORDINAL1:def 13;
A2: mid f,k1,k2 = (f | k21) /^ (k11 -' 1) by AB540b;
k1 >= 0 + 1 by A6, NAT_1:13;
then A17: k1 -' 1 = k1 - 1 by XREAL_1:235;
k1 >= k2 + 1 by A6, NAT_1:13;
then A18: k1 - 1 >= (k2 + 1) - 1 by XREAL_1:11;
len (f | k21) <= k21 by TH80f;
hence mid f,k1,k2 = {} by A2, TH80e, A17, A18, XXREAL_0:2; :: thesis: verum