let n be Element of NAT ; :: thesis: 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); :: thesis: ( C is connected implies N-min C in right_cell (Cage C,n),1 )
assume A1: C is connected ; :: thesis: N-min C in right_cell (Cage C,n),1
then consider i being Element of NAT such that
A2: ( 1 <= i & i + 1 <= len (Gauge C,n) ) and
A3: (Cage C,n) /. 1 = (Gauge C,n) * i,(width (Gauge C,n)) and
A4: (Cage C,n) /. 2 = (Gauge C,n) * (i + 1),(width (Gauge C,n)) and
A5: 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;
A6: 1 + 1 <= len (Cage C,n) by GOBOARD7:36, XXREAL_0:2;
for i1, j1, i2, j2 being Element of 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

let i1, j1, i2, j2 be Element of NAT ; :: thesis: ( [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
A7: [i1,j1] in Indices (GoB (Cage C,n)) and
A8: [i2,j2] in Indices (GoB (Cage C,n)) and
A9: (Cage C,n) /. 1 = (GoB (Cage C,n)) * i1,j1 and
A10: (Cage C,n) /. (1 + 1) = (GoB (Cage C,n)) * i2,j2 ; :: thesis: ( ( 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 ) )
A11: GoB (Cage C,n) = Gauge C,n by A1, Th52;
0 <> width (Gauge C,n) by GOBOARD1:def 5;
then A12: 1 <= width (Gauge C,n) by NAT_1:14;
i < len (Gauge C,n) by A2, NAT_1:13;
then A13: [i,(width (Gauge C,n))] in Indices (Gauge C,n) by A2, A12, MATRIX_1:37;
then A14: ( i1 = i & j1 = width (Gauge C,n) ) by A3, A7, A9, A11, GOBOARD1:21;
1 <= i + 1 by NAT_1:11;
then [(i + 1),(width (Gauge C,n))] in Indices (Gauge C,n) by A2, A12, MATRIX_1:37;
then A15: ( i2 = i + 1 & j2 = width (Gauge C,n) ) by A4, A8, A10, A11, GOBOARD1:21;

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 A3, A7, A9, A11, A13, A15, GOBOARD1:21;

case ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) = cell (GoB (Cage C,n)),i1,j1

hence cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) = cell (GoB (Cage C,n)),i1,j1 by A14, A15; :: thesis: verum

end;

case ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: 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 A1, A14, Th52; :: thesis: verum

end;

case ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) = cell (GoB (Cage C,n)),i2,j2

hence cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) = cell (GoB (Cage C,n)),i2,j2 by A14, A15; :: thesis: verum

end;

case ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) = cell (GoB (Cage C,n)),(i1 -' 1),j2

hence cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) = cell (GoB (Cage C,n)),(i1 -' 1),j2 by A14, A15; :: thesis: verum

end;

end;

end;

hence N-min C in right_cell (Cage C,n),1 by A5, A6, GOBOARD5:def 6; :: thesis: verum