let n be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
n >= 1
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( n is_sufficiently_large_for C implies n >= 1 )
assume n is_sufficiently_large_for C ; :: thesis: n >= 1
then consider j being Element of NAT such that
A1: j < width (Gauge C,n) and
A2: cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C by Def3;
A3: width (Gauge C,n) = (2 |^ n) + 3 by JORDAN1A:49;
A4: j > 1

proof

A5: (X-SpanStart C,n) -' 1 <= len (Gauge C,n) by Th59;
assume A6: j <= 1 ; :: thesis: contradiction

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

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

0 <= width (Gauge C,n) ;
then A8: not cell (Gauge C,n),((X-SpanStart C,n) -' 1),0 is empty by A5, JORDAN1A:45;
cell (Gauge C,n),((X-SpanStart C,n) -' 1),0 c= UBD C by A5, JORDAN1A:70;
hence contradiction by A2, A7, A8, JORDAN2C:28, XBOOLE_1:68; :: thesis: verum

end;

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

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

end;

end;

end;

A19: j + 1 < width (Gauge C,n)

proof

A20: (X-SpanStart C,n) -' 1 <= len (Gauge C,n) by Th59;
assume j + 1 >= width (Gauge C,n) ; :: thesis: contradiction
then A21: ( 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 A1, A21, NAT_1:13;

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

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

end;

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

then A24: cell (Gauge C,n),((X-SpanStart C,n) -' 1),((width (Gauge C,n)) -' 1) c= BDD C by A2, NAT_D:34;
(width (Gauge C,n)) -' 1 <= width (Gauge C,n) by NAT_D:44;
then A25: not cell (Gauge C,n),((X-SpanStart C,n) -' 1),((width (Gauge C,n)) -' 1) is empty by A20, JORDAN1A:45;
A26: cell (Gauge C,n),((X-SpanStart C,n) -' 1),(width (Gauge C,n)) c= UBD C by A20, JORDAN1A:71;
set i1 = X-SpanStart C,n;
A27: X-SpanStart C,n < len (Gauge C,n) by Th58;
A28: width (Gauge C,n) <> 0 by GOBOARD1:def 5;
(X-SpanStart C,n) -' 1 <= X-SpanStart C,n by NAT_D:44;
then A29: (X-SpanStart C,n) -' 1 < len (Gauge C,n) by A27, XXREAL_0:2;
A30: (width (Gauge C,n)) - 1 < width (Gauge C,n) by XREAL_1:148;
then A31: (width (Gauge C,n)) -' 1 < width (Gauge C,n) by A28, NAT_1:14, XREAL_1:235;
A32: ((width (Gauge C,n)) -' 1) + 1 = width (Gauge C,n) by A28, NAT_1:14, XREAL_1:237;
1 <= (X-SpanStart C,n) -' 1 by Th59;
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 A29, A30, A32, GOBOARD5:27;
then A33: 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:73, JORDAN2C:76;
then A34: 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 A24, XBOOLE_1:1;
then cell (Gauge C,n),((X-SpanStart C,n) -' 1),((width (Gauge C,n)) -' 1) c= UBD C by A26, A29, A31, A33, A34, GOBOARD9:6, JORDAN1A:46;
hence contradiction by A24, A25, JORDAN2C:28, XBOOLE_1:68; :: thesis: verum

end;

end;

end;

A35: 2 |^ 0 = 1 by NEWTON:9;
assume n < 1 ; :: thesis: contradiction
then A36: n = 0 by NAT_1:14;
then A37: j <= 3 + 1 by A1, A3, NEWTON:9;

per cases ( j = 0 or j = 1 or j = 2 or j = 3 or j = 4 ) by A37, NAT_1:29;

suppose ( j = 0 or j = 1 ) ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose A38: j = 2 ; :: thesis: contradiction

A39: X-SpanStart C,0 = 1 + 2 by A35, NAT_2:10;
then (X-SpanStart C,0 ) -' 1 = (X-SpanStart C,0 ) - 1 by NAT_D:39
.= 2 by A39 ;
hence contradiction by A2, A36, A38, JORDAN1B:19; :: thesis: verum

end;

suppose ( j = 3 or j = 4 ) ; :: thesis: contradiction

hence contradiction by A3, A19, A35, A36; :: thesis: verum

end;

end;