let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds (Lower_Seq C,n) /. 1 = E-max (L~ (Cage C,n))
let n be Element of NAT ; :: thesis: (Lower_Seq C,n) /. 1 = E-max (L~ (Cage C,n))
Lower_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) :- (E-max (L~ (Cage C,n))) by JORDAN1E:def 2;
hence (Lower_Seq C,n) /. 1 = E-max (L~ (Cage C,n)) by FINSEQ_5:56; :: thesis: verum