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
( 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); :: thesis: ( 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
; :: thesis: ( 1 < Y-SpanStart C,n & Y-SpanStart C,n <= width (Gauge C,n) )
thus
1 < Y-SpanStart C,n
:: thesis: Y-SpanStart C,n <= width (Gauge C,n)proof
A2:
(X-SpanStart C,n) -' 1
<= len (Gauge C,n)
by JORDAN1H:59;
assume A3:
Y-SpanStart C,
n <= 1
;
:: thesis: contradiction
per cases
( Y-SpanStart C,n = 0 or Y-SpanStart C,n = 1 )
by A3, NAT_1:26;
suppose
Y-SpanStart C,
n = 0
;
:: thesis: contradictionthen A4:
cell (Gauge C,n),
((X-SpanStart C,n) -' 1),
0 c= BDD C
by A1, Th6;
0 <= width (Gauge C,n)
;
then A5:
not
cell (Gauge C,n),
((X-SpanStart C,n) -' 1),
0 is
empty
by A2, JORDAN1A:45;
cell (Gauge C,n),
((X-SpanStart C,n) -' 1),
0 c= UBD C
by A2, JORDAN1A:70;
hence
contradiction
by A4, A5, JORDAN2C:28, XBOOLE_1:68;
:: thesis: verum end; suppose
Y-SpanStart C,
n = 1
;
:: thesis: contradictionthen A6:
cell (Gauge C,n),
((X-SpanStart C,n) -' 1),1
c= BDD C
by A1, Th6;
A7:
width (Gauge C,n) <> 0
by GOBOARD1:def 5;
then A8:
0 + 1
<= width (Gauge C,n)
by NAT_1:14;
then A9:
not
cell (Gauge C,n),
((X-SpanStart C,n) -' 1),1 is
empty
by A2, JORDAN1A:45;
A10:
cell (Gauge C,n),
((X-SpanStart C,n) -' 1),
0 c= UBD C
by A2, JORDAN1A:70;
set i1 =
X-SpanStart C,
n;
A11:
X-SpanStart C,
n < len (Gauge C,n)
by JORDAN1H:58;
(X-SpanStart C,n) -' 1
<= X-SpanStart C,
n
by NAT_D:44;
then A12:
(X-SpanStart C,n) -' 1
< len (Gauge C,n)
by A11, XXREAL_0:2;
A13:
0 < width (Gauge C,n)
by A7;
1
<= (X-SpanStart C,n) -' 1
by JORDAN1H:59;
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, A13, GOBOARD5:27;
then A14:
cell (Gauge C,n),
((X-SpanStart C,n) -' 1),
0 meets cell (Gauge C,n),
((X-SpanStart C,n) -' 1),
(0 + 1)
by XBOOLE_0:def 7;
UBD C is_outside_component_of C
by JORDAN2C:76;
then A15:
UBD C is_a_component_of C `
by JORDAN2C:def 4;
BDD C c= C `
by JORDAN2C:29;
then
cell (Gauge C,n),
((X-SpanStart C,n) -' 1),1
c= C `
by A6, XBOOLE_1:1;
then
cell (Gauge C,n),
((X-SpanStart C,n) -' 1),1
c= UBD C
by A8, A10, A12, A14, A15, GOBOARD9:6, JORDAN1A:46;
hence
contradiction
by A6, A9, JORDAN2C:28, XBOOLE_1:68;
:: thesis: verum end;
end;
thus
Y-SpanStart C,n <= width (Gauge C,n)
by A1, Def3; :: thesis: verum