theorem :: SPRECT_2:23

for f being non trivial FinSequence of (TOP-REAL 2)
for i, j being Nat st i in dom f & j in dom f holds
mid (f,i,j) is_in_the_area_of f by Th21, Th22;