let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT st ex i, j being Element of NAT st
( i <= len (Gauge C,n) & j <= width (Gauge C,n) & cell (Gauge C,n),i,j c= BDD C ) holds
n >= 1
let n be Element of NAT ; :: thesis: ( ex i, j being Element of NAT st
( i <= len (Gauge C,n) & j <= width (Gauge C,n) & cell (Gauge C,n),i,j c= BDD C ) implies n >= 1 )
given i, j being Element of NAT such that A1: i <= len (Gauge C,n) and
A2: j <= width (Gauge C,n) and
A3: cell (Gauge C,n),i,j c= BDD C ; :: thesis: n >= 1
A4: width (Gauge C,n) = (2 |^ n) + 3 by JORDAN1A:49;
A5: len (Gauge C,n) = (2 |^ n) + 3 by JORDAN8:def 1;
A6: j + 1 < width (Gauge C,n) by A1, A2, A3, Th42;
A7: i + 1 < len (Gauge C,n) by A1, A2, A3, Th43;
A8: 2 |^ 0 = 1 by NEWTON:9;
assume A9: n < 1 ; :: thesis: contradiction
then A10: width (Gauge C,n) = 1 + 3 by A4, A8, NAT_1:14;
A11: len (Gauge C,n) = 1 + 3 by A5, A8, A9, NAT_1:14;

per cases ( j = 0 or j = 1 or i = 0 or i = 1 or ( j = 2 & i = 2 ) or j = 3 or j = 4 or i = 3 or i = 4 ) by A1, A2, A10, A11, NAT_1:29;

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

hence contradiction by A1, A2, A3, Th40; :: thesis: verum

end;

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

hence contradiction by A1, A2, A3, Th41; :: thesis: verum

end;

suppose ( j = 2 & i = 2 ) ; :: thesis: contradiction

then cell (Gauge C,0 ),2,2 c= BDD C by A3, A9, NAT_1:14;
hence contradiction by Th19; :: thesis: verum

end;

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

hence contradiction by A6, A7, A10, A11; :: thesis: verum

end;

end;