let n be 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 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; :: 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_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 = 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:5; :: 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:34, XXREAL_0:2;
hence N-min C in right_cell ((Cage (C,n)),1) by A6, A7, GOBOARD5:def 6; :: thesis: verum