let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: Y-InitStart C > 1
set m = ApproxIndex C;
A1:
(X-SpanStart C,(ApproxIndex C)) -' 1 <= len (Gauge C,(ApproxIndex C))
by JORDAN1H:59;
assume A2:
Y-InitStart C <= 1
; :: thesis: contradiction
per cases
( Y-InitStart C = 0 or Y-InitStart C = 1 )
by A2, NAT_1:26;
suppose
Y-InitStart C = 0
;
:: thesis: contradictionthen A3:
cell (Gauge C,(ApproxIndex C)),
((X-SpanStart C,(ApproxIndex C)) -' 1),
0 c= BDD C
by Def2;
0 <= width (Gauge C,(ApproxIndex C))
;
then A4:
not
cell (Gauge C,(ApproxIndex C)),
((X-SpanStart C,(ApproxIndex C)) -' 1),
0 is
empty
by A1, JORDAN1A:45;
cell (Gauge C,(ApproxIndex C)),
((X-SpanStart C,(ApproxIndex C)) -' 1),
0 c= UBD C
by A1, JORDAN1A:70;
hence
contradiction
by A3, A4, JORDAN2C:28, XBOOLE_1:68;
:: thesis: verum end; suppose
Y-InitStart C = 1
;
:: thesis: contradictionthen A5:
cell (Gauge C,(ApproxIndex C)),
((X-SpanStart C,(ApproxIndex C)) -' 1),1
c= BDD C
by Def2;
A6:
width (Gauge C,(ApproxIndex C)) <> 0
by GOBOARD1:def 5;
then A7:
0 + 1
<= width (Gauge C,(ApproxIndex C))
by NAT_1:14;
then A8:
not
cell (Gauge C,(ApproxIndex C)),
((X-SpanStart C,(ApproxIndex C)) -' 1),1 is
empty
by A1, JORDAN1A:45;
A9:
cell (Gauge C,(ApproxIndex C)),
((X-SpanStart C,(ApproxIndex C)) -' 1),
0 c= UBD C
by A1, JORDAN1A:70;
set i1 =
X-SpanStart C,
(ApproxIndex C);
A10:
X-SpanStart C,
(ApproxIndex C) < len (Gauge C,(ApproxIndex C))
by JORDAN1H:58;
(X-SpanStart C,(ApproxIndex C)) -' 1
<= X-SpanStart C,
(ApproxIndex C)
by NAT_D:44;
then A11:
(X-SpanStart C,(ApproxIndex C)) -' 1
< len (Gauge C,(ApproxIndex C))
by A10, XXREAL_0:2;
A12:
0 < width (Gauge C,(ApproxIndex C))
by A6;
1
<= (X-SpanStart C,(ApproxIndex C)) -' 1
by JORDAN1H:59;
then
(cell (Gauge C,(ApproxIndex C)),((X-SpanStart C,(ApproxIndex C)) -' 1),0 ) /\ (cell (Gauge C,(ApproxIndex C)),((X-SpanStart C,(ApproxIndex C)) -' 1),(0 + 1)) = LSeg ((Gauge C,(ApproxIndex C)) * ((X-SpanStart C,(ApproxIndex C)) -' 1),(0 + 1)),
((Gauge C,(ApproxIndex C)) * (((X-SpanStart C,(ApproxIndex C)) -' 1) + 1),(0 + 1))
by A11, A12, GOBOARD5:27;
then A13:
cell (Gauge C,(ApproxIndex C)),
((X-SpanStart C,(ApproxIndex C)) -' 1),
0 meets cell (Gauge C,(ApproxIndex C)),
((X-SpanStart C,(ApproxIndex C)) -' 1),
(0 + 1)
by XBOOLE_0:def 7;
UBD C is_outside_component_of C
by JORDAN2C:76;
then A14:
UBD C is_a_component_of C `
by JORDAN2C:def 4;
BDD C c= C `
by JORDAN2C:29;
then
cell (Gauge C,(ApproxIndex C)),
((X-SpanStart C,(ApproxIndex C)) -' 1),1
c= C `
by A5, XBOOLE_1:1;
then
cell (Gauge C,(ApproxIndex C)),
((X-SpanStart C,(ApproxIndex C)) -' 1),1
c= UBD C
by A7, A9, A11, A13, A14, GOBOARD9:6, JORDAN1A:46;
hence
contradiction
by A5, A8, JORDAN2C:28, XBOOLE_1:68;
:: thesis: verum end;