let n be Element of NAT ; :: thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
Y-SpanStart C,n <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2
let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: ( n is_sufficiently_large_for C implies Y-SpanStart C,n <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 )
set m = ApproxIndex C;
A1: X-SpanStart C,(ApproxIndex C) > 2 by JORDAN1H:58;
assume A2: n is_sufficiently_large_for C ; :: thesis: Y-SpanStart C,n <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2
then A3: n >= ApproxIndex C by Def1;
set i1 = X-SpanStart C,n;
set j0 = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2;
A4: (Y-InitStart C) + 1 < width (Gauge C,(ApproxIndex C)) by Th3;
A5: 1 < Y-InitStart C by Th2;
then 1 + 1 <= Y-InitStart C by NAT_1:13;
then A6: (Y-InitStart C) -' 2 = (Y-InitStart C) - 2 by XREAL_1:235;
Y-InitStart C < (Y-InitStart C) + 1 by XREAL_1:31;
then Y-InitStart C < width (Gauge C,(ApproxIndex C)) by Th3, XXREAL_0:2;
then A7: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= width (Gauge C,n) by A3, A5, A6, JORDAN1A:53;

now

let j be Element of NAT ; :: thesis: ( ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= j & j <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 implies cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C )
assume ( ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= j & j <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 ) ; :: thesis: cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C
then A8: j = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by XXREAL_0:1;
A9: cell (Gauge C,(ApproxIndex C)),((X-SpanStart C,(ApproxIndex C)) -' 1),(Y-InitStart C) c= BDD C by Def2;
A10: 2 + 1 <= X-SpanStart C,(ApproxIndex C) by A1, NAT_1:13;
A11: len (Gauge C,(ApproxIndex C)) = (2 |^ (ApproxIndex C)) + 3 by JORDAN8:def 1;
(ApproxIndex C) -' 1 <= ApproxIndex C by NAT_D:44;
then 2 |^ ((ApproxIndex C) -' 1) <= 2 |^ (ApproxIndex C) by PREPOWER:107;
then A12: X-SpanStart C,(ApproxIndex C) < len (Gauge C,(ApproxIndex C)) by A11, XREAL_1:10;
X-SpanStart C,n = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart C,(ApproxIndex C)) - 2)) + 2 by A2, Th4;
then cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= cell (Gauge C,(ApproxIndex C)),((X-SpanStart C,(ApproxIndex C)) -' 1),(Y-InitStart C) by A3, A4, A6, A8, A10, A12, Th2, JORDAN1A:69;
hence cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C by A9, XBOOLE_1:1; :: thesis: verum

end;

hence Y-SpanStart C,n <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A2, A7, Def3; :: thesis: verum