let f be non trivial FinSequence of (TOP-REAL 2); :: thesis: <*(SW-corner (L~ f))*> is_in_the_area_of f
set g = <*(SW-corner (L~ f))*>;
let n be Nat; :: according to SPRECT_2:def 1 :: thesis: ( n in dom <*(SW-corner (L~ f))*> implies ( W-bound (L~ f) <= (<*(SW-corner (L~ f))*> /. n) `1 & (<*(SW-corner (L~ f))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(SW-corner (L~ f))*> /. n) `2 & (<*(SW-corner (L~ f))*> /. n) `2 <= N-bound (L~ f) ) )
assume A1: n in dom <*(SW-corner (L~ f))*> ; :: thesis: ( W-bound (L~ f) <= (<*(SW-corner (L~ f))*> /. n) `1 & (<*(SW-corner (L~ f))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(SW-corner (L~ f))*> /. n) `2 & (<*(SW-corner (L~ f))*> /. n) `2 <= N-bound (L~ f) )
dom <*(SW-corner (L~ f))*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then n = 1 by A1, TARSKI:def 1;
then <*(SW-corner (L~ f))*> /. n = |[(W-bound (L~ f)),(S-bound (L~ f))]| by FINSEQ_4:16;
then ( (<*(SW-corner (L~ f))*> /. n) `1 = W-bound (L~ f) & (<*(SW-corner (L~ f))*> /. n) `2 = S-bound (L~ f) ) by EUCLID:52;
hence ( W-bound (L~ f) <= (<*(SW-corner (L~ f))*> /. n) `1 & (<*(SW-corner (L~ f))*> /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (<*(SW-corner (L~ f))*> /. n) `2 & (<*(SW-corner (L~ f))*> /. n) `2 <= N-bound (L~ f) ) by SPRECT_1:21, SPRECT_1:22; :: thesis: verum