let n be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage C,n))) .. (Lower_Seq C,n) = 1
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: (E-max (L~ (Cage C,n))) .. (Lower_Seq C,n) = 1
(Lower_Seq C,n) /. 1 = E-max (L~ (Cage C,n)) by JORDAN1F:6;
hence (E-max (L~ (Cage C,n))) .. (Lower_Seq C,n) = 1 by FINSEQ_6:47; :: thesis: verum