:: deftheorem defines is_in_the_area_of SPRECT_2:def 1 :
for f, g being FinSequence of (TOP-REAL 2) holds
( g is_in_the_area_of f iff for n being Nat st n in dom g holds
( W-bound (L~ f) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ f) ) );