:: deftheorem defines is_a_v.c._for SPRECT_2:def 3 :
for f, g being FinSequence of (TOP-REAL 2) holds
( g is_a_v.c._for f iff ( g is_in_the_area_of f & (g /. 1) `2 = S-bound (L~ f) & (g /. (len g)) `2 = N-bound (L~ f) ) );