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

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