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_a_h.c._for Cage C,n
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: Upper_Seq C,n is_a_h.c._for Cage C,n
A1: Upper_Seq C,n is_in_the_area_of Cage C,n by JORDAN1E:21;
A2: ((Upper_Seq C,n) /. 1) `1 = (W-min (L~ (Cage C,n))) `1 by JORDAN1F:5
.= W-bound (L~ (Cage C,n)) by EUCLID:56 ;
((Upper_Seq C,n) /. (len (Upper_Seq C,n))) `1 = (E-max (L~ (Cage C,n))) `1 by JORDAN1F:7
.= E-bound (L~ (Cage C,n)) by EUCLID:56 ;
hence Upper_Seq C,n is_a_h.c._for Cage C,n by A1, A2, SPRECT_2:def 2; :: thesis: verum