let i, j be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds
N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( i < j implies N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i))) )
assume A1: i < j ; :: thesis: N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i)))
defpred S₁[ Nat] means ( i < $1 implies N-bound (L~ (Cage (C,$1))) < N-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 = N-bound C;
set s = S-bound C;
A4: ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ (n + 1)))) - ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))) = (0 + (((N-bound C) - (S-bound C)) / (2 |^ (n + 1)))) - (((N-bound C) - (S-bound C)) / (2 |^ n))
.= (((N-bound C) - (S-bound C)) / ((2 |^ n) * 2)) - ((((N-bound C) - (S-bound C)) / (2 |^ n)) / (2 / 2)) by NEWTON:6
.= (((N-bound C) - (S-bound C)) / ((2 |^ n) * 2)) - ((((N-bound C) - (S-bound C)) * 2) / ((2 |^ n) * 2)) by XCMPLX_1:84
.= (((N-bound C) - (S-bound C)) - ((2 * (N-bound C)) - (2 * (S-bound C)))) / ((2 |^ n) * 2) by XCMPLX_1:120
.= ((S-bound C) - (N-bound C)) / ((2 |^ n) * 2) ;
2 |^ n > 0 by NEWTON:83;
then A5: (2 |^ n) * 2 > 0 * 2 by XREAL_1:68;
A6: ( N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) & N-bound (L~ (Cage (C,(n + 1)))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ (n + 1))) ) by Th6;
(S-bound C) - (N-bound C) < 0 by SPRECT_1:32, XREAL_1:49;
then 0 > ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ (n + 1)))) - ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))) by A5, A4, XREAL_1:141;
then A7: N-bound (L~ (Cage (C,(n + 1)))) < N-bound (L~ (Cage (C,n))) by A6, XREAL_1:48;
assume i < n + 1 ; :: thesis: N-bound (L~ (Cage (C,(n + 1)))) < N-bound (L~ (Cage (C,i)))
then i <= n by NAT_1:13;
hence N-bound (L~ (Cage (C,(n + 1)))) < N-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 N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i))) by A1; :: thesis: verum