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
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 )
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
and
A4:
j <= 1
; contradiction
per cases
( j = 0 or j = 1 )
by A4, NAT_1:25;
suppose A5:
j = 1
;
contradiction
BDD C c= C `
by JORDAN2C:25;
then A6:
cell (
(Gauge (C,n)),
i,1)
c= C `
by A3, A5;
A7:
i <> 0
by A2, A3, Lm3;
UBD C is_outside_component_of C
by JORDAN2C:68;
then A8:
UBD C is_a_component_of C `
by JORDAN2C:def 3;
A9:
width (Gauge (C,n)) <> 0
by MATRIX_0:def 10;
then A10:
0 + 1
<= width (Gauge (C,n))
by NAT_1:14;
then A11:
not
cell (
(Gauge (C,n)),
i,1) is
empty
by A1, JORDAN1A:24;
i < len (Gauge (C,n))
by A1, A2, A3, Lm5, XXREAL_0:1;
then
(cell ((Gauge (C,n)),i,0)) /\ (cell ((Gauge (C,n)),i,(0 + 1))) = LSeg (
((Gauge (C,n)) * (i,(0 + 1))),
((Gauge (C,n)) * ((i + 1),(0 + 1))))
by A9, A7, GOBOARD5:26, NAT_1:14;
then A12:
cell (
(Gauge (C,n)),
i,
0)
meets cell (
(Gauge (C,n)),
i,
(0 + 1))
by XBOOLE_0:def 7;
cell (
(Gauge (C,n)),
i,
0)
c= UBD C
by A1, JORDAN1A:49;
then
cell (
(Gauge (C,n)),
i,1)
c= UBD C
by A1, A10, A12, A8, A6, GOBOARD9:4, JORDAN1A:25;
hence
contradiction
by A3, A5, A11, JORDAN2C:24, XBOOLE_1:68;
verum end; end;