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