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 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 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

0 <> width (Gauge C,n) by GOBOARD1:def 5;
then A8: 1 <= width (Gauge C,n) by NAT_1:14;
A9: GoB (Cage C,n) = Gauge C,n by A1, Th52;
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
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 ; :: 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 ) )
1 <= i + 1 by NAT_1:11;
then A14: [(i + 1),(width (Gauge C,n))] in Indices (Gauge C,n) by A3, A8, MATRIX_1:37;
then A15: i2 = i + 1 by A5, A11, A13, A9, GOBOARD1:21;
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_1:37;
then A17: i1 = i by A4, A10, A12, A9, GOBOARD1:21;
A18: j2 = width (Gauge C,n) by A5, A11, A13, A9, A14, 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 A4, A10, A12, A9, A16, A15, A18, 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 A17, 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 A4, A10, A12, A9, A16, A17, GOBOARD1:21; :: 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 A17, 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 A17, A15; :: thesis: verum

end;

end;

end;

1 + 1 <= len (Cage C,n) by GOBOARD7:36, XXREAL_0:2;
hence N-min C in right_cell (Cage C,n),1 by A6, A7, GOBOARD5:def 6; :: thesis: verum