let i, j be Nat; 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); ( i < j implies S-bound (L~ (Cage (C,i))) < S-bound (L~ (Cage (C,j))) )
assume A1:
i < j
; S-bound (L~ (Cage (C,i))) < S-bound (L~ (Cage (C,j)))
defpred S1[ Nat] means ( i < $1 implies S-bound (L~ (Cage (C,i))) < S-bound (L~ (Cage (C,$1))) );
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[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
;
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;
verum
end;
A8:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A8, A2);
hence
S-bound (L~ (Cage (C,i))) < S-bound (L~ (Cage (C,j)))
by A1; verum