let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n, m being Element of NAT st n <= m & n is_sufficiently_large_for C holds
m is_sufficiently_large_for C
let n, m be Element of NAT ; :: thesis: ( n <= m & n is_sufficiently_large_for C implies m is_sufficiently_large_for C )
assume that
A1: n <= m and
A2: n is_sufficiently_large_for C ; :: thesis: m is_sufficiently_large_for C
consider j being Element of NAT such that
A3: j < width (Gauge C,n) and
A4: cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C by A2, JORDAN1H:def 3;
set iim = X-SpanStart C,m;
set iin = X-SpanStart C,n;
n >= 1 by A2, JORDAN1H:60;
then A5: X-SpanStart C,m = ((2 |^ (m -' n)) * ((X-SpanStart C,n) - 2)) + 2 by A1, Th28;
X-SpanStart C,n > 2 by JORDAN1H:58;
then A6: X-SpanStart C,n >= 2 + 1 by NAT_1:13;
A7: X-SpanStart C,n < len (Gauge C,n) by JORDAN1H:58;
A8: j > 1

proof

A9: (X-SpanStart C,n) -' 1 <= len (Gauge C,n) by JORDAN1H:59;
assume A10: j <= 1 ; :: thesis: contradiction

per cases ( j = 0 or j = 1 ) by A10, NAT_1:26;

suppose A11: j = 0 ; :: thesis: contradiction

width (Gauge C,n) >= 0 by NAT_1:2;
then A12: not cell (Gauge C,n),((X-SpanStart C,n) -' 1),0 is empty by A9, JORDAN1A:45;
cell (Gauge C,n),((X-SpanStart C,n) -' 1),0 c= UBD C by A9, JORDAN1A:70;
hence contradiction by A4, A11, A12, JORDAN2C:28, XBOOLE_1:68; :: thesis: verum

end;

suppose A13: j = 1 ; :: thesis: contradiction

width (Gauge C,n) <> 0 by GOBOARD1:def 5;
then A14: 0 + 1 <= width (Gauge C,n) by NAT_1:14;
then A15: not cell (Gauge C,n),((X-SpanStart C,n) -' 1),1 is empty by A9, JORDAN1A:45;
A16: cell (Gauge C,n),((X-SpanStart C,n) -' 1),0 c= UBD C by A9, JORDAN1A:70;
set i1 = X-SpanStart C,n;
A17: 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 A18: (X-SpanStart C,n) -' 1 < len (Gauge C,n) by A17, XXREAL_0:2;
A19: 0 < width (Gauge C,n) by A14, NAT_1:13;
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 A18, A19, GOBOARD5:27;
then A20: 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 A21: 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 A4, A13, XBOOLE_1:1;
then cell (Gauge C,n),((X-SpanStart C,n) -' 1),1 c= UBD C by A14, A16, A18, A20, A21, GOBOARD9:6, JORDAN1A:46;
hence contradiction by A4, A13, A15, JORDAN2C:28, XBOOLE_1:68; :: thesis: verum

end;

end;

end;

then ((2 |^ (m -' n)) * (j - 2)) + 2 > 1 by A1, A3, JORDAN1A:53;
then reconsider j1 = ((2 |^ (m -' n)) * (j - 2)) + 2 as Element of NAT by INT_1:16, XXREAL_0:2;
A22: j1 < width (Gauge C,m) by A1, A3, A8, JORDAN1A:53;
j + 1 < width (Gauge C,n)

proof

A23: (X-SpanStart C,n) -' 1 <= len (Gauge C,n) by JORDAN1H:59;
assume j + 1 >= width (Gauge C,n) ; :: thesis: contradiction
then A24: ( j + 1 > width (Gauge C,n) or j + 1 = width (Gauge C,n) ) by XXREAL_0:1;

per cases ( j = width (Gauge C,n) or j + 1 = width (Gauge C,n) ) by A3, A24, NAT_1:13;

suppose A25: j = width (Gauge C,n) ; :: thesis: contradiction

then A26: not cell (Gauge C,n),((X-SpanStart C,n) -' 1),j is empty by A23, JORDAN1A:45;
cell (Gauge C,n),((X-SpanStart C,n) -' 1),(width (Gauge C,n)) c= UBD C by A23, JORDAN1A:71;
hence contradiction by A4, A25, A26, JORDAN2C:28, XBOOLE_1:68; :: thesis: verum

end;

suppose j + 1 = width (Gauge C,n) ; :: thesis: contradiction

then A27: cell (Gauge C,n),((X-SpanStart C,n) -' 1),((width (Gauge C,n)) -' 1) c= BDD C by A4, NAT_D:34;
(width (Gauge C,n)) -' 1 <= width (Gauge C,n) by NAT_D:44;
then A28: not cell (Gauge C,n),((X-SpanStart C,n) -' 1),((width (Gauge C,n)) -' 1) is empty by A23, JORDAN1A:45;
A29: cell (Gauge C,n),((X-SpanStart C,n) -' 1),(width (Gauge C,n)) c= UBD C by A23, JORDAN1A:71;
set i1 = X-SpanStart C,n;
A30: X-SpanStart C,n < len (Gauge C,n) by JORDAN1H:58;
A31: width (Gauge C,n) <> 0 by GOBOARD1:def 5;
(X-SpanStart C,n) -' 1 <= X-SpanStart C,n by NAT_D:44;
then A32: (X-SpanStart C,n) -' 1 < len (Gauge C,n) by A30, XXREAL_0:2;
A33: (width (Gauge C,n)) - 1 < width (Gauge C,n) by XREAL_1:148;
then A34: (width (Gauge C,n)) -' 1 < width (Gauge C,n) by A31, NAT_1:14, XREAL_1:235;
A35: ((width (Gauge C,n)) -' 1) + 1 = width (Gauge C,n) by A31, NAT_1:14, XREAL_1:237;
1 <= (X-SpanStart C,n) -' 1 by JORDAN1H:59;
then (cell (Gauge C,n),((X-SpanStart C,n) -' 1),(width (Gauge C,n))) /\ (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((width (Gauge C,n)) -' 1)) = LSeg ((Gauge C,n) * ((X-SpanStart C,n) -' 1),(width (Gauge C,n))),((Gauge C,n) * (((X-SpanStart C,n) -' 1) + 1),(width (Gauge C,n))) by A32, A33, A35, GOBOARD5:27;
then A36: cell (Gauge C,n),((X-SpanStart C,n) -' 1),(width (Gauge C,n)) meets cell (Gauge C,n),((X-SpanStart C,n) -' 1),((width (Gauge C,n)) -' 1) by XBOOLE_0:def 7;
UBD C is_outside_component_of C by JORDAN2C:76;
then A37: 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),((width (Gauge C,n)) -' 1) c= C ` by A27, XBOOLE_1:1;
then cell (Gauge C,n),((X-SpanStart C,n) -' 1),((width (Gauge C,n)) -' 1) c= UBD C by A29, A32, A34, A36, A37, GOBOARD9:6, JORDAN1A:46;
hence contradiction by A27, A28, JORDAN2C:28, XBOOLE_1:68; :: thesis: verum

end;

end;

end;

then cell (Gauge C,m),((X-SpanStart C,m) -' 1),j1 c= cell (Gauge C,n),((X-SpanStart C,n) -' 1),j by A1, A5, A6, A7, A8, JORDAN1A:69;
then cell (Gauge C,m),((X-SpanStart C,m) -' 1),j1 c= BDD C by A4, XBOOLE_1:1;
hence m is_sufficiently_large_for C by A22, JORDAN1H:def 3; :: thesis: verum