for f being FinSequence of (TOP-REAL 2)
for k1, k2 being Element of NAT st f is being_S-Seq & 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & k1 <> k2 holds
mid (f,k1,k2) is being_S-Seq