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
cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) -' 1) meets C
let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: ( n is_sufficiently_large_for C implies cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) -' 1) meets C )
assume A1: n is_sufficiently_large_for C ; :: thesis: cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) -' 1) meets C
set i1 = X-SpanStart C,n;
A2: Y-SpanStart C,n <= width (Gauge C,n) by A1, Def3;
assume A3: cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) -' 1) misses C ; :: thesis: contradiction
A4: (Y-SpanStart C,n) -' 1 <= width (Gauge C,n) by A2, NAT_D:44;
A5: 1 < Y-SpanStart C,n by A1, Th7;
for k being Element of NAT st (Y-SpanStart C,n) -' 1 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
cell (Gauge C,n),((X-SpanStart C,n) -' 1),k c= BDD C

proof

let k be Element of NAT ; :: thesis: ( (Y-SpanStart C,n) -' 1 <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 implies cell (Gauge C,n),((X-SpanStart C,n) -' 1),k c= BDD C )
assume that
A6: (Y-SpanStart C,n) -' 1 <= k and
A7: k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 ; :: thesis: cell (Gauge C,n),((X-SpanStart C,n) -' 1),k c= BDD C

per cases ( (Y-SpanStart C,n) -' 1 = k or (Y-SpanStart C,n) -' 1 < k ) by A6, XXREAL_0:1;

suppose A8: (Y-SpanStart C,n) -' 1 = k ; :: thesis: cell (Gauge C,n),((X-SpanStart C,n) -' 1),k c= BDD C

then A9: cell (Gauge C,n),((X-SpanStart C,n) -' 1),k c= C ` by A3, SUBSET_1:43;
A10: X-SpanStart C,n < len (Gauge C,n) by JORDAN1H:58;
(X-SpanStart C,n) -' 1 <= X-SpanStart C,n by NAT_D:44;
then A11: (X-SpanStart C,n) -' 1 < len (Gauge C,n) by A10, XXREAL_0:2;
A12: ( 1 < Y-SpanStart C,n & Y-SpanStart C,n <= width (Gauge C,n) ) by A1, Th7;
then A13: k + 1 = Y-SpanStart C,n by A8, XREAL_1:237;
k < k + 1 by XREAL_1:31;
then A14: k < width (Gauge C,n) by A12, A13, XXREAL_0:2;
1 + 1 < X-SpanStart C,n by JORDAN1H:58;
then 1 <= (X-SpanStart C,n) - 1 by XREAL_1:21;
then 1 <= (X-SpanStart C,n) -' 1 by NAT_D:39;
then (cell (Gauge C,n),((X-SpanStart C,n) -' 1),k) /\ (cell (Gauge C,n),((X-SpanStart C,n) -' 1),(k + 1)) = LSeg ((Gauge C,n) * ((X-SpanStart C,n) -' 1),(k + 1)),((Gauge C,n) * (((X-SpanStart C,n) -' 1) + 1),(k + 1)) by A11, A14, GOBOARD5:27;
then cell (Gauge C,n),((X-SpanStart C,n) -' 1),k meets cell (Gauge C,n),((X-SpanStart C,n) -' 1),(k + 1) by XBOOLE_0:def 7;
then A15: cell (Gauge C,n),((X-SpanStart C,n) -' 1),k meets BDD C by A1, A13, Th6, XBOOLE_1:63;
set W = { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } ;
A16: BDD C = union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } by JORDAN2C:def 5;
then consider e being set such that
A17: e in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } and
A18: cell (Gauge C,n),((X-SpanStart C,n) -' 1),k meets e by A15, ZFMISC_1:98;
consider B being Subset of (TOP-REAL 2) such that
A19: e = B and
A20: B is_inside_component_of C by A17;
B is_a_component_of C ` by A20, JORDAN2C:def 3;
then A21: cell (Gauge C,n),((X-SpanStart C,n) -' 1),k c= B by A9, A11, A14, A18, A19, GOBOARD9:6, JORDAN1A:46;
B c= BDD C by A16, A17, A19, ZFMISC_1:92;
hence cell (Gauge C,n),((X-SpanStart C,n) -' 1),k c= BDD C by A21, XBOOLE_1:1; :: thesis: verum

end;

suppose (Y-SpanStart C,n) -' 1 < k ; :: thesis: cell (Gauge C,n),((X-SpanStart C,n) -' 1),k c= BDD C

then Y-SpanStart C,n < k + 1 by NAT_D:55;
then Y-SpanStart C,n <= k by NAT_1:13;
hence cell (Gauge C,n),((X-SpanStart C,n) -' 1),k c= BDD C by A1, A7, Def3; :: thesis: verum

end;

end;

end;

then A22: (Y-SpanStart C,n) -' 1 >= Y-SpanStart C,n by A1, A4, Def3;
(Y-SpanStart C,n) - 1 < Y-SpanStart C,n by XREAL_1:148;
hence contradiction by A5, A22, XREAL_1:235; :: thesis: verum