let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds ((Cage (C,n)) /. 2) `2 = N-bound (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ((Cage (C,n)) /. 2) `2 = N-bound (L~ (Cage (C,n)))
(Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then (Cage (C,n)) /. 2 in N-most (L~ (Cage (C,n))) by SPRECT_2:30;
then ((Cage (C,n)) /. 2) `2 = (N-min (L~ (Cage (C,n)))) `2 by PSCOMP_1:39;
hence ((Cage (C,n)) /. 2) `2 = N-bound (L~ (Cage (C,n))) by EUCLID:52; :: thesis: verum