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 )
A1: 2 |^ 0 = 1 by NEWTON:4;
given i, j being Element of NAT such that A2: i <= len (Gauge (C,n)) and
A3: j <= width (Gauge (C,n)) and
A4: cell ((Gauge (C,n)),i,j) c= BDD C ; :: thesis: n >= 1
A5: j + 1 < width (Gauge (C,n)) by A2, A3, A4, Th42;
A6: i + 1 < len (Gauge (C,n)) by A2, A3, A4, Th43;
assume A7: n < 1 ; :: thesis: contradiction
len (Gauge (C,n)) = (2 |^ n) + 3 by JORDAN8:def 1;
then A8: len (Gauge (C,n)) = 1 + 3 by A1, A7, NAT_1:14;
width (Gauge (C,n)) = (2 |^ n) + 3 by JORDAN1A:28;
then A9: width (Gauge (C,n)) = 1 + 3 by A1, A7, 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 A2, A3, A9, A8, NAT_1:28;

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

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

end;

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

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

end;

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

then cell ((Gauge (C,0)),2,2) c= BDD C by A4, A7, 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 A5, A6, A9, A8; :: thesis: verum

end;

end;