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 ;

( 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;

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;hence contradiction by Th18; :: thesis: verum