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