let n be Nat; for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds
N-min C in right_cell ((Cage (C,n)),1)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ( C is connected implies N-min C in right_cell ((Cage (C,n)),1) )
assume A1:
C is connected
; N-min C in right_cell ((Cage (C,n)),1)
then consider i being Nat such that
A2:
1 <= i
and
A3:
i + 1 <= len (Gauge (C,n))
and
A4:
(Cage (C,n)) /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n))))
and
A5:
(Cage (C,n)) /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n))))
and
A6:
N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1))
and
N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1))
by JORDAN9:def 1;
A7:
for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB (Cage (C,n))) & [i2,j2] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. 1 = (GoB (Cage (C,n))) * (i1,j1) & (Cage (C,n)) /. (1 + 1) = (GoB (Cage (C,n))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2) )
proof
0 <> width (Gauge (C,n))
by MATRIX_0:def 10;
then A8:
1
<= width (Gauge (C,n))
by NAT_1:14;
A9:
GoB (Cage (C,n)) = Gauge (
C,
n)
by A1, Th44;
let i1,
j1,
i2,
j2 be
Nat;
( [i1,j1] in Indices (GoB (Cage (C,n))) & [i2,j2] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. 1 = (GoB (Cage (C,n))) * (i1,j1) & (Cage (C,n)) /. (1 + 1) = (GoB (Cage (C,n))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2) ) implies ( i1 = i2 & j1 = j2 + 1 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2) ) )
assume that A10:
[i1,j1] in Indices (GoB (Cage (C,n)))
and A11:
[i2,j2] in Indices (GoB (Cage (C,n)))
and A12:
(Cage (C,n)) /. 1
= (GoB (Cage (C,n))) * (
i1,
j1)
and A13:
(Cage (C,n)) /. (1 + 1) = (GoB (Cage (C,n))) * (
i2,
j2)
;
( ( i1 = i2 & j1 + 1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2) ) )
1
<= i + 1
by NAT_1:11;
then A14:
[(i + 1),(width (Gauge (C,n)))] in Indices (Gauge (C,n))
by A3, A8, MATRIX_0:30;
then A15:
i2 = i + 1
by A5, A11, A13, A9, GOBOARD1:5;
i < len (Gauge (C,n))
by A3, NAT_1:13;
then A16:
[i,(width (Gauge (C,n)))] in Indices (Gauge (C,n))
by A2, A8, MATRIX_0:30;
then A17:
i1 = i
by A4, A10, A12, A9, GOBOARD1:5;
A18:
j2 = width (Gauge (C,n))
by A5, A11, A13, A9, A14, GOBOARD1:5;
per cases
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A4, A10, A12, A9, A16, A15, A18, GOBOARD1:5;
case
(
i1 + 1
= i2 &
j1 = j2 )
;
cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1))thus
cell (
(Gauge (C,n)),
i,
((width (Gauge (C,n))) -' 1))
= cell (
(GoB (Cage (C,n))),
i1,
(j1 -' 1))
by A4, A10, A12, A9, A16, A17, GOBOARD1:5;
verum end; end;
end;
1 + 1 <= len (Cage (C,n))
by GOBOARD7:34, XXREAL_0:2;
hence
N-min C in right_cell ((Cage (C,n)),1)
by A6, A7, GOBOARD5:def 6; verum