let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); 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; ( 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
; 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
; 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 = 2 &
i = 2 )
;
contradictionend; suppose
(
j = 3 or
j = 4 or
i = 3 or
i = 4 )
;
contradictionhence
contradiction
by A5, A6, A9, A8;
verum end; end;