let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat st ex i, j being 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 Nat; :: thesis: ( ex i, j being 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 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, Th39;
A6: i + 1 < len (Gauge (C,n)) by A2, A3, A4, Th40;
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;
i <= 4 by A8, A2;
then A10: not not i = 0 & ... & not i = 4 ;
j <= 4 by A3, A9;
then not not j = 0 & ... & not j = 4 ;
per cases then ( 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 A10;
suppose ( j = 0 or j = 1 ) ; :: thesis: contradiction
hence contradiction by A2, A3, A4, Th37; :: thesis: verum
end;
suppose ( i = 0 or i = 1 ) ; :: thesis: contradiction
hence contradiction by A2, A3, A4, Th38; :: 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 Th18; :: 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;