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