let f be non trivial FinSequence of (TOP-REAL 2); :: thesis: f is_in_the_area_of f
let n be Nat; :: according to SPRECT_2:def 1 :: thesis: ( n in dom f implies ( W-bound (L~ f) <= (f /. n) `1 & (f /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (f /. n) `2 & (f /. n) `2 <= N-bound (L~ f) ) )
assume A1: n in dom f ; :: thesis: ( W-bound (L~ f) <= (f /. n) `1 & (f /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (f /. n) `2 & (f /. n) `2 <= N-bound (L~ f) )
len f >= 2 by NAT_D:60;
then f /. n in L~ f by A1, GOBOARD1:1;
hence ( W-bound (L~ f) <= (f /. n) `1 & (f /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (f /. n) `2 & (f /. n) `2 <= N-bound (L~ f) ) by PSCOMP_1:24; :: thesis: verum