let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for i, j, n being Nat st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j + 1 < width (Gauge (C,n))
let i, j, n be Nat; ( i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies j + 1 < width (Gauge (C,n)) )
assume 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
; j + 1 < width (Gauge (C,n))
A4:
( j < width (Gauge (C,n)) or j = width (Gauge (C,n)) )
by A2, XXREAL_0:1;
assume
j + 1 >= width (Gauge (C,n))
; contradiction
then A5:
( j + 1 > width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) )
by XXREAL_0:1;
per cases
( j = width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) )
by A5, A4, NAT_1:13;
suppose
j + 1
= width (Gauge (C,n))
;
contradictionthen A6:
cell (
(Gauge (C,n)),
i,
((width (Gauge (C,n))) -' 1))
c= BDD C
by A3, NAT_D:34;
BDD C c= C `
by JORDAN2C:25;
then A7:
cell (
(Gauge (C,n)),
i,
((width (Gauge (C,n))) -' 1))
c= C `
by A6;
A8:
width (Gauge (C,n)) <> 0
by MATRIX_0:def 10;
then A9:
((width (Gauge (C,n))) -' 1) + 1
= width (Gauge (C,n))
by NAT_1:14, XREAL_1:235;
(width (Gauge (C,n))) -' 1
<= width (Gauge (C,n))
by NAT_D:44;
then A10:
not
cell (
(Gauge (C,n)),
i,
((width (Gauge (C,n))) -' 1)) is
empty
by A1, JORDAN1A:24;
A11:
cell (
(Gauge (C,n)),
i,
(width (Gauge (C,n))))
c= UBD C
by A1, JORDAN1A:50;
UBD C is_outside_component_of C
by JORDAN2C:68;
then A12:
UBD C is_a_component_of C `
by JORDAN2C:def 3;
A13:
i <> 0
by A2, A3, Lm3;
A14:
(width (Gauge (C,n))) - 1
< width (Gauge (C,n))
by XREAL_1:146;
i < len (Gauge (C,n))
by A1, A2, A3, Lm5, XXREAL_0:1;
then
(cell ((Gauge (C,n)),i,(width (Gauge (C,n))))) /\ (cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1))) = LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((Gauge (C,n)) * ((i + 1),(width (Gauge (C,n))))))
by A14, A9, A13, GOBOARD5:26, NAT_1:14;
then A15:
cell (
(Gauge (C,n)),
i,
(width (Gauge (C,n))))
meets cell (
(Gauge (C,n)),
i,
((width (Gauge (C,n))) -' 1))
by XBOOLE_0:def 7;
(width (Gauge (C,n))) -' 1
< width (Gauge (C,n))
by A8, A14, NAT_1:14, XREAL_1:233;
then
cell (
(Gauge (C,n)),
i,
((width (Gauge (C,n))) -' 1))
c= UBD C
by A1, A11, A15, A12, A7, GOBOARD9:4, JORDAN1A:25;
hence
contradiction
by A6, A10, JORDAN2C:24, XBOOLE_1:68;
verum end; end;