let n be Element of 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:34;
then (Cage C,n) /. 2 in N-most (L~ (Cage C,n)) by SPRECT_2:34;
then ((Cage C,n) /. 2) `2 = (N-min (L~ (Cage C,n))) `2 by PSCOMP_1:98;
hence ((Cage C,n) /. 2) `2 = N-bound (L~ (Cage C,n)) by EUCLID:56; :: thesis: verum