let n be 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:146;
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 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 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:235;
A10: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= C ` by A4, A8, SUBSET_1:23;
A11: k < k + 1 by XREAL_1:29;
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:49;
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 4;
1 + 1 < X-SpanStart (C,n) by JORDAN1H:49;
then 1 <= (X-SpanStart (C,n)) - 1 by XREAL_1:19;
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:26;
then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) meets cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(k + 1)) ;
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:80;
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:74;
B is_a_component_of C ` by A19, JORDAN2C:def 2;
then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= B by A10, A14, A12, A17, A18, GOBOARD9:4, JORDAN1A:25;
hence cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),k) c= BDD C by A20; :: 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:233; :: thesis: verum