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:49;
set j0 = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2;
set i1 = X-SpanStart (C,n);
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;
A4: 1 < Y-InitStart C by Th2;
then 1 + 1 <= Y-InitStart C by NAT_1:13;
then A5: (Y-InitStart C) -' 2 = (Y-InitStart C) - 2 by XREAL_1:233;
A6: (Y-InitStart C) + 1 < width (Gauge (C,(ApproxIndex C))) by Th3;

A7: now

(ApproxIndex C) -' 1 <= ApproxIndex C by NAT_D:44;
then A8: 2 |^ ((ApproxIndex C) -' 1) <= 2 |^ (ApproxIndex C) by PREPOWER:93;
len (Gauge (C,(ApproxIndex C))) = (2 |^ (ApproxIndex C)) + 3 by JORDAN8:def 1;
then A9: X-SpanStart (C,(ApproxIndex C)) < len (Gauge (C,(ApproxIndex C))) by A8, XREAL_1:8;
A10: 2 + 1 <= X-SpanStart (C,(ApproxIndex C)) by A1, NAT_1:13;
A11: X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 by A2, Th4;
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 that
A12: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= j and
A13: j <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 ; :: thesis: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C
A14: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(Y-InitStart C)) c= BDD C by Def2;
j = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A12, A13, XXREAL_0:1;
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, A6, A5, A10, A9, A11, Th2, JORDAN1A:48;
hence cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C by A14, XBOOLE_1:1; :: thesis: verum

end;

Y-InitStart C < (Y-InitStart C) + 1 by XREAL_1:29;
then Y-InitStart C < width (Gauge (C,(ApproxIndex C))) by Th3, XXREAL_0:2;
then ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= width (Gauge (C,n)) by A3, A4, A5, JORDAN1A:32;
hence Y-SpanStart (C,n) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A2, A7, Def3; :: thesis: verum