let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-bound C < E-bound (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: E-bound C < E-bound (L~ (Cage (C,n)))
A1: 2 |^ n > 0 by NEWTON:83;
E-bound C > (W-bound C) + 0 by SPRECT_1:31;
then (E-bound C) - (W-bound C) > 0 by XREAL_1:20;
then A2: ((E-bound C) - (W-bound C)) / (2 |^ n) > (E-bound C) - (E-bound C) by A1, XREAL_1:139;
E-bound (L~ (Cage (C,n))) = (E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by JORDAN1A:64;
hence E-bound C < E-bound (L~ (Cage (C,n))) by A2, XREAL_1:19; :: thesis: verum