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