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 )
set i1 = X-SpanStart C,n;
A1: (Y-SpanStart C,n) - 1 < Y-SpanStart C,n by XREAL_1:148;
assume A2: n is_sufficiently_large_for C ; :: thesis: cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) -' 1) meets C
then A3: 1 < Y-SpanStart C,n by Th7;
assume A4: cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) -' 1) misses C ; :: thesis: contradiction
A5: 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

1 < Y-SpanStart C,n by A2, Th7;
then A9: k + 1 = Y-SpanStart C,n by A8, XREAL_1:237;
A10: cell (Gauge C,n),((X-SpanStart C,n) -' 1),k c= C ` by A4, A8, SUBSET_1:43;
A11: k < k + 1 by XREAL_1:31;
Y-SpanStart C,n <= width (Gauge C,n) by A2, Th7;
then A12: k < width (Gauge C,n) by A9, A11, XXREAL_0:2;
set W = { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } ;
A13: (X-SpanStart C,n) -' 1 <= X-SpanStart C,n by NAT_D:44;
X-SpanStart C,n < len (Gauge C,n) by JORDAN1H:58;
then A14: (X-SpanStart C,n) -' 1 < len (Gauge C,n) by A13, XXREAL_0:2;
A15: BDD C = union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } by JORDAN2C:def 5;
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 A14, A12, 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 cell (Gauge C,n),((X-SpanStart C,n) -' 1),k meets BDD C by A2, A9, Th6, XBOOLE_1:63;
then consider e being set such that
A16: e in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } and
A17: 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
A18: e = B and
A19: B is_inside_component_of C by A16;
A20: B c= BDD C by A15, A16, A18, ZFMISC_1:92;
B is_a_component_of C ` by A19, JORDAN2C:def 3;
then cell (Gauge C,n),((X-SpanStart C,n) -' 1),k c= B by A10, A14, A12, A17, A18, GOBOARD9:6, JORDAN1A:46;
hence cell (Gauge C,n),((X-SpanStart C,n) -' 1),k c= BDD C by A20, 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 A2, A7, Def3; :: thesis: verum

end;

end;

end;

Y-SpanStart C,n <= width (Gauge C,n) by A2, Def3;
then (Y-SpanStart C,n) -' 1 <= width (Gauge C,n) by NAT_D:44;
then (Y-SpanStart C,n) -' 1 >= Y-SpanStart C,n by A2, A5, Def3;
hence contradiction by A3, A1, XREAL_1:235; :: thesis: verum