let n be Nat; 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); 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; verum