let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: (Y-InitStart C) + 1 < width (Gauge (C,(ApproxIndex C)))
set m = ApproxIndex C;
A1: (X-SpanStart (C,(ApproxIndex C))) -' 1 <= len (Gauge (C,(ApproxIndex C))) by JORDAN1H:50;
assume (Y-InitStart C) + 1 >= width (Gauge (C,(ApproxIndex C))) ; :: thesis: contradiction
then A2: ( (Y-InitStart C) + 1 > width (Gauge (C,(ApproxIndex C))) or (Y-InitStart C) + 1 = width (Gauge (C,(ApproxIndex C))) ) by XXREAL_0:1;
A3: ( Y-InitStart C < width (Gauge (C,(ApproxIndex C))) or Y-InitStart C = width (Gauge (C,(ApproxIndex C))) ) by Def2;

per cases ( Y-InitStart C = width (Gauge (C,(ApproxIndex C))) or (Y-InitStart C) + 1 = width (Gauge (C,(ApproxIndex C))) ) by A2, A3, NAT_1:13;

suppose Y-InitStart C = width (Gauge (C,(ApproxIndex C))) ; :: thesis: contradiction

hence contradiction by Def2; :: thesis: verum

end;

suppose (Y-InitStart C) + 1 = width (Gauge (C,(ApproxIndex C))) ; :: thesis: contradiction

then Y-InitStart C = (width (Gauge (C,(ApproxIndex C)))) -' 1 by NAT_D:34;
then A4: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),((width (Gauge (C,(ApproxIndex C)))) -' 1)) c= BDD C by Def2;
BDD C c= C ` by JORDAN2C:25;
then A5: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),((width (Gauge (C,(ApproxIndex C)))) -' 1)) c= C ` by A4;
A6: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(width (Gauge (C,(ApproxIndex C))))) c= UBD C by A1, JORDAN1A:50;
set i1 = X-SpanStart (C,(ApproxIndex C));
A7: (X-SpanStart (C,(ApproxIndex C))) -' 1 <= X-SpanStart (C,(ApproxIndex C)) by NAT_D:44;
X-SpanStart (C,(ApproxIndex C)) < len (Gauge (C,(ApproxIndex C))) by JORDAN1H:49;
then A8: (X-SpanStart (C,(ApproxIndex C))) -' 1 < len (Gauge (C,(ApproxIndex C))) by A7, XXREAL_0:2;
UBD C is_outside_component_of C by JORDAN2C:68;
then A9: UBD C is_a_component_of C ` by JORDAN2C:def 3;
(width (Gauge (C,(ApproxIndex C)))) -' 1 <= width (Gauge (C,(ApproxIndex C))) by NAT_D:44;
then A10: not cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),((width (Gauge (C,(ApproxIndex C)))) -' 1)) is empty by A1, JORDAN1A:24;
A11: (width (Gauge (C,(ApproxIndex C)))) - 1 < width (Gauge (C,(ApproxIndex C))) by XREAL_1:146;
A12: 1 <= (X-SpanStart (C,(ApproxIndex C))) -' 1 by JORDAN1H:50;
A13: width (Gauge (C,(ApproxIndex C))) <> 0 by MATRIX_0:def 10;
then ((width (Gauge (C,(ApproxIndex C)))) -' 1) + 1 = width (Gauge (C,(ApproxIndex C))) by NAT_1:14, XREAL_1:235;
then (cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(width (Gauge (C,(ApproxIndex C)))))) /\ (cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),((width (Gauge (C,(ApproxIndex C)))) -' 1))) = LSeg (((Gauge (C,(ApproxIndex C))) * (((X-SpanStart (C,(ApproxIndex C))) -' 1),(width (Gauge (C,(ApproxIndex C)))))),((Gauge (C,(ApproxIndex C))) * ((((X-SpanStart (C,(ApproxIndex C))) -' 1) + 1),(width (Gauge (C,(ApproxIndex C))))))) by A8, A11, A12, GOBOARD5:26;
then A14: cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),(width (Gauge (C,(ApproxIndex C))))) meets cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),((width (Gauge (C,(ApproxIndex C)))) -' 1)) ;
(width (Gauge (C,(ApproxIndex C)))) -' 1 < width (Gauge (C,(ApproxIndex C))) by A13, A11, NAT_1:14, XREAL_1:233;
then cell ((Gauge (C,(ApproxIndex C))),((X-SpanStart (C,(ApproxIndex C))) -' 1),((width (Gauge (C,(ApproxIndex C)))) -' 1)) c= UBD C by A6, A8, A14, A9, A5, GOBOARD9:4, JORDAN1A:25;
hence contradiction by A4, A10, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum

end;

end;