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