let n be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq C,n is_in_the_area_of Cage C,n
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: Lower_Seq C,n is_in_the_area_of Cage C,n
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
hence Lower_Seq C,n is_in_the_area_of Cage C,n by Th6, JORDAN1B:11; :: thesis: verum