let n be 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:43; :: thesis: verum

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:43; :: thesis: verum