let n be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_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: Upper_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 Upper_Seq C,n is_in_the_area_of Cage C,n by Th5, JORDAN1B:11; :: thesis: verum