let n be Nat; for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
( 1 < Y-SpanStart (C,n) & Y-SpanStart (C,n) <= width (Gauge (C,n)) )
let C be being_simple_closed_curve Subset of (TOP-REAL 2); ( n is_sufficiently_large_for C implies ( 1 < Y-SpanStart (C,n) & Y-SpanStart (C,n) <= width (Gauge (C,n)) ) )
assume A1:
n is_sufficiently_large_for C
; ( 1 < Y-SpanStart (C,n) & Y-SpanStart (C,n) <= width (Gauge (C,n)) )
thus
1 < Y-SpanStart (C,n)
Y-SpanStart (C,n) <= width (Gauge (C,n))proof
A2:
(X-SpanStart (C,n)) -' 1
<= len (Gauge (C,n))
by JORDAN1H:50;
assume A3:
Y-SpanStart (
C,
n)
<= 1
;
contradiction
per cases
( Y-SpanStart (C,n) = 0 or Y-SpanStart (C,n) = 1 )
by A3, NAT_1:25;
suppose A4:
Y-SpanStart (
C,
n)
= 0
;
contradictionA5:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0)
c= UBD C
by A2, JORDAN1A:49;
0 <= width (Gauge (C,n))
;
then A6:
not
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0) is
empty
by A2, JORDAN1A:24;
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0)
c= BDD C
by A1, A4, Th6;
hence
contradiction
by A6, A5, JORDAN2C:24, XBOOLE_1:68;
verum end; suppose
Y-SpanStart (
C,
n)
= 1
;
contradictionthen A7:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),1)
c= BDD C
by A1, Th6;
set i1 =
X-SpanStart (
C,
n);
A8:
(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 A9:
(X-SpanStart (C,n)) -' 1
< len (Gauge (C,n))
by A8, XXREAL_0:2;
BDD C c= C `
by JORDAN2C:25;
then A10:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),1)
c= C `
by A7;
UBD C is_outside_component_of C
by JORDAN2C:68;
then A11:
UBD C is_a_component_of C `
by JORDAN2C:def 3;
A12:
width (Gauge (C,n)) <> 0
by MATRIX_0:def 10;
then A13:
0 + 1
<= width (Gauge (C,n))
by NAT_1:14;
then A14:
not
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),1) is
empty
by A2, JORDAN1A:24;
1
<= (X-SpanStart (C,n)) -' 1
by JORDAN1H:50;
then
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0)) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1))) = LSeg (
((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(0 + 1))),
((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(0 + 1))))
by A12, A9, GOBOARD5:26;
then A15:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0)
meets cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
(0 + 1))
;
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0)
c= UBD C
by A2, JORDAN1A:49;
then
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),1)
c= UBD C
by A13, A9, A15, A11, A10, GOBOARD9:4, JORDAN1A:25;
hence
contradiction
by A7, A14, JORDAN2C:24, XBOOLE_1:68;
verum end; end;
end;
thus
Y-SpanStart (C,n) <= width (Gauge (C,n))
by A1, Def3; verum