let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound C < N-bound (L~ (Cage (C,n)))

let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: N-bound C < N-bound (L~ (Cage (C,n)))

A1: 2 |^ n > 0 by NEWTON:83;

N-bound C > (S-bound C) + 0 by SPRECT_1:32;

then (N-bound C) - (S-bound C) > 0 by XREAL_1:20;

then A2: ((N-bound C) - (S-bound C)) / (2 |^ n) > (N-bound C) - (N-bound C) by A1, XREAL_1:139;

N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) by JORDAN10:6;

hence N-bound C < N-bound (L~ (Cage (C,n))) by A2, XREAL_1:19; :: thesis: verum

let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: N-bound C < N-bound (L~ (Cage (C,n)))

A1: 2 |^ n > 0 by NEWTON:83;

N-bound C > (S-bound C) + 0 by SPRECT_1:32;

then (N-bound C) - (S-bound C) > 0 by XREAL_1:20;

then A2: ((N-bound C) - (S-bound C)) / (2 |^ n) > (N-bound C) - (N-bound C) by A1, XREAL_1:139;

N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) by JORDAN10:6;

hence N-bound C < N-bound (L~ (Cage (C,n))) by A2, XREAL_1:19; :: thesis: verum