let f be non trivial FinSequence of (TOP-REAL 2); :: thesis: <*(SE-corner (L~ f))*> is_in_the_area_of f
set g = <*(SE-corner (L~ f))*>;
let n be Element of NAT ; :: according to SPRECT_2:def 1 :: thesis: ( n in dom <*(SE-corner (L~ f))*> implies ( W-bound (L~ f) <= (<*(SE-corner (L~ f))*> /. n) `1 & (<*(SE-corner (L~ f))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(SE-corner (L~ f))*> /. n) `2 & (<*(SE-corner (L~ f))*> /. n) `2 <= N-bound (L~ f) ) )
A1: dom <*(SE-corner (L~ f))*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
assume n in dom <*(SE-corner (L~ f))*> ; :: thesis: ( W-bound (L~ f) <= (<*(SE-corner (L~ f))*> /. n) `1 & (<*(SE-corner (L~ f))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(SE-corner (L~ f))*> /. n) `2 & (<*(SE-corner (L~ f))*> /. n) `2 <= N-bound (L~ f) )
then n = 1 by A1, TARSKI:def 1;
then <*(SE-corner (L~ f))*> /. n = |[(E-bound (L~ f)),(S-bound (L~ f))]| by FINSEQ_4:25;
then ( (<*(SE-corner (L~ f))*> /. n) `1 = E-bound (L~ f) & (<*(SE-corner (L~ f))*> /. n) `2 = S-bound (L~ f) ) by EUCLID:56;
hence ( W-bound (L~ f) <= (<*(SE-corner (L~ f))*> /. n) `1 & (<*(SE-corner (L~ f))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(SE-corner (L~ f))*> /. n) `2 & (<*(SE-corner (L~ f))*> /. n) `2 <= N-bound (L~ f) ) by SPRECT_1:23, SPRECT_1:24; :: thesis: verum