let n be 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))) /. 1) `1 = ((Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))) `1 by FINSEQ_5:65

.= (W-min (L~ (Cage (C,n)))) `1 by JORDAN1F:8

.= W-bound (L~ (Cage (C,n))) by EUCLID:52 ;

A2: ((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:65

.= (E-max (L~ (Cage (C,n)))) `1 by JORDAN1F:6

.= E-bound (L~ (Cage (C,n))) by EUCLID:52 ;

Rev (Lower_Seq (C,n)) is_in_the_area_of Cage (C,n) by JORDAN1E:18, SPRECT_3:51;

hence Rev (Lower_Seq (C,n)) is_a_h.c._for Cage (C,n) by A1, A2, SPRECT_2:def 2; :: thesis: verum

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))) /. 1) `1 = ((Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))) `1 by FINSEQ_5:65

.= (W-min (L~ (Cage (C,n)))) `1 by JORDAN1F:8

.= W-bound (L~ (Cage (C,n))) by EUCLID:52 ;

A2: ((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:65

.= (E-max (L~ (Cage (C,n)))) `1 by JORDAN1F:6

.= E-bound (L~ (Cage (C,n))) by EUCLID:52 ;

Rev (Lower_Seq (C,n)) is_in_the_area_of Cage (C,n) by JORDAN1E:18, SPRECT_3:51;

hence Rev (Lower_Seq (C,n)) is_a_h.c._for Cage (C,n) by A1, A2, SPRECT_2:def 2; :: thesis: verum