for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f holds
for i, j being Nat st i in dom g & j in dom g holds
mid (g,i,j) is_in_the_area_of f