let n be 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)) /. 1) `1 = (W-min (L~ (Cage (C,n)))) `1 by JORDAN1F:5
.= W-bound (L~ (Cage (C,n))) by EUCLID:52 ;
A2: ((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:52 ;
Upper_Seq (C,n) is_in_the_area_of Cage (C,n) by JORDAN1E:17;
hence Upper_Seq (C,n) is_a_h.c._for Cage (C,n) by A1, A2, SPRECT_2:def 2; :: thesis: verum