let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n, m being Nat st n <= m & n is_sufficiently_large_for C holds
m is_sufficiently_large_for C
let n, m be 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 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 iin = X-SpanStart (C,n);
set iim = X-SpanStart (C,m);
n >= 1 by A2, JORDAN1H:51;
then A5: X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 by A1, Th27;
A6: j > 1

proof

A7: (X-SpanStart (C,n)) -' 1 <= len (Gauge (C,n)) by JORDAN1H:50;
assume A8: j <= 1 ; :: thesis: contradiction

per cases ( j = 0 or j = 1 ) by A8, NAT_1:25;

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

width (Gauge (C,n)) >= 0 ;
then A10: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) is empty by A7, JORDAN1A:24;
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A7, JORDAN1A:49;
hence contradiction by A4, A9, A10, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum

end;

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

set i1 = X-SpanStart (C,n);
A12: (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 A13: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by A12, XXREAL_0:2;
BDD C c= C ` by JORDAN2C:25;
then A14: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= C ` by A4, A11;
UBD C is_outside_component_of C by JORDAN2C:68;
then A15: UBD C is_a_component_of C ` by JORDAN2C:def 3;
width (Gauge (C,n)) <> 0 by MATRIX_0:def 10;
then A16: 0 + 1 <= width (Gauge (C,n)) by NAT_1:14;
then A17: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) is empty by A7, JORDAN1A:24;
A18: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50;
0 < width (Gauge (C,n)) by A16;
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 A13, A18, GOBOARD5:26;
then A19: 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;
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A7, JORDAN1A:49;
then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= UBD C by A16, A13, A19, A15, A14, GOBOARD9:4, JORDAN1A:25;
hence contradiction by A4, A11, A17, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum

end;

end;

end;

then ((2 |^ (m -' n)) * (j - 2)) + 2 > 1 by A1, A3, JORDAN1A:32;
then reconsider j1 = ((2 |^ (m -' n)) * (j - 2)) + 2 as Element of NAT by INT_1:3;
X-SpanStart (C,n) > 2 by JORDAN1H:49;
then A20: X-SpanStart (C,n) >= 2 + 1 by NAT_1:13;
A21: j + 1 < width (Gauge (C,n))

proof

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

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

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

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

end;

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

then A26: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= BDD C by A4, NAT_D:34;
BDD C c= C ` by JORDAN2C:25;
then A27: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= C ` by A26;
A28: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) c= UBD C by A23, JORDAN1A:50;
set i1 = X-SpanStart (C,n);
A29: (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 A30: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by A29, XXREAL_0:2;
UBD C is_outside_component_of C by JORDAN2C:68;
then A31: UBD C is_a_component_of C ` by JORDAN2C:def 3;
(width (Gauge (C,n))) -' 1 <= width (Gauge (C,n)) by NAT_D:44;
then A32: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) is empty by A23, JORDAN1A:24;
A33: (width (Gauge (C,n))) - 1 < width (Gauge (C,n)) by XREAL_1:146;
A34: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50;
A35: width (Gauge (C,n)) <> 0 by MATRIX_0:def 10;
then ((width (Gauge (C,n))) -' 1) + 1 = width (Gauge (C,n)) by NAT_1:14, XREAL_1:235;
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 A30, A33, A34, GOBOARD5:26;
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;
(width (Gauge (C,n))) -' 1 < width (Gauge (C,n)) by A35, A33, NAT_1:14, XREAL_1:233;
then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= UBD C by A28, A30, A36, A31, A27, GOBOARD9:4, JORDAN1A:25;
hence contradiction by A26, A32, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum

end;

end;

end;

X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49;
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, A20, A6, A21, JORDAN1A:48;
then A37: cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),j1) c= BDD C by A4;
j1 < width (Gauge (C,m)) by A1, A3, A6, JORDAN1A:32;
hence m is_sufficiently_large_for C by A37, JORDAN1H:def 3; :: thesis: verum