let n be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Rev (Lower_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: Rev (Lower_Seq C,n) is_a_h.c._for Cage C,n
A1: Rev (Lower_Seq C,n) is_in_the_area_of Cage C,n by JORDAN1E:22, SPRECT_3:68;
A2: ((Rev (Lower_Seq C,n)) /. 1) `1 = ((Lower_Seq C,n) /. (len (Lower_Seq C,n))) `1 by FINSEQ_5:68
.= (W-min (L~ (Cage C,n))) `1 by JORDAN1F:8
.= W-bound (L~ (Cage C,n)) by EUCLID:56 ;
((Rev (Lower_Seq C,n)) /. (len (Rev (Lower_Seq C,n)))) `1 = ((Rev (Lower_Seq C,n)) /. (len (Lower_Seq C,n))) `1 by FINSEQ_5:def 3
.= ((Lower_Seq C,n) /. 1) `1 by FINSEQ_5:68
.= (E-max (L~ (Cage C,n))) `1 by JORDAN1F:6
.= E-bound (L~ (Cage C,n)) by EUCLID:56 ;
hence Rev (Lower_Seq C,n) is_a_h.c._for Cage C,n by A1, A2, SPRECT_2:def 2; :: thesis: verum