let i, j be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds
E-bound (L~ (Cage (C,j))) < E-bound (L~ (Cage (C,i)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( i < j implies E-bound (L~ (Cage (C,j))) < E-bound (L~ (Cage (C,i))) )
assume A1: i < j ; :: thesis: E-bound (L~ (Cage (C,j))) < E-bound (L~ (Cage (C,i)))
defpred S₁[ Nat] means ( i < $1 implies E-bound (L~ (Cage (C,$1))) < E-bound (L~ (Cage (C,i))) );
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
set j = n + 1;
set a = E-bound C;
set s = W-bound C;
A4: ((E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ (n + 1)))) - ((E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n))) = (0 + (((E-bound C) - (W-bound C)) / (2 |^ (n + 1)))) - (((E-bound C) - (W-bound C)) / (2 |^ n))
.= (((E-bound C) - (W-bound C)) / ((2 |^ n) * 2)) - ((((E-bound C) - (W-bound C)) / (2 |^ n)) / (2 / 2)) by NEWTON:6
.= (((E-bound C) - (W-bound C)) / ((2 |^ n) * 2)) - ((((E-bound C) - (W-bound C)) * 2) / ((2 |^ n) * 2)) by XCMPLX_1:84
.= (((E-bound C) - (W-bound C)) - ((2 * (E-bound C)) - (2 * (W-bound C)))) / ((2 |^ n) * 2) by XCMPLX_1:120
.= ((W-bound C) - (E-bound C)) / ((2 |^ n) * 2) ;
2 |^ n > 0 by NEWTON:83;
then A5: (2 |^ n) * 2 > 0 * 2 by XREAL_1:68;
A6: ( E-bound (L~ (Cage (C,n))) = (E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n)) & E-bound (L~ (Cage (C,(n + 1)))) = (E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ (n + 1))) ) by Th64;
(W-bound C) - (E-bound C) < 0 by SPRECT_1:31, XREAL_1:49;
then 0 > ((E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ (n + 1)))) - ((E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n))) by A5, A4, XREAL_1:141;
then A7: E-bound (L~ (Cage (C,(n + 1)))) < E-bound (L~ (Cage (C,n))) by A6, XREAL_1:48;
assume i < n + 1 ; :: thesis: E-bound (L~ (Cage (C,(n + 1)))) < E-bound (L~ (Cage (C,i)))
then i <= n by NAT_1:13;
hence E-bound (L~ (Cage (C,(n + 1)))) < E-bound (L~ (Cage (C,i))) by A3, A7, XXREAL_0:1, XXREAL_0:2; :: thesis: verum

end;

A8: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A8, A2);
hence E-bound (L~ (Cage (C,j))) < E-bound (L~ (Cage (C,i))) by A1; :: thesis: verum