let i, j be Element of NAT ; :: thesis: for f being non constant standard special_circular_sequence st 1 <= i & i < len (GoB f) & 1 <= j & j + 1 < width (GoB f) & LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 1),(j + 1)) c= L~ f & LSeg ((GoB f) * (i + 1),(j + 1)),((GoB f) * (i + 1),(j + 2)) c= L~ f holds
not LSeg ((GoB f) * i,(j + 1)),((GoB f) * (i + 1),(j + 1)) c= L~ f
let f be non constant standard special_circular_sequence; :: thesis: ( 1 <= i & i < len (GoB f) & 1 <= j & j + 1 < width (GoB f) & LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 1),(j + 1)) c= L~ f & LSeg ((GoB f) * (i + 1),(j + 1)),((GoB f) * (i + 1),(j + 2)) c= L~ f implies not LSeg ((GoB f) * i,(j + 1)),((GoB f) * (i + 1),(j + 1)) c= L~ f )
assume that
A1: ( 1 <= i & i < len (GoB f) ) and
A2: ( 1 <= j & j + 1 < width (GoB f) ) and
A3: LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 1),(j + 1)) c= L~ f and
A4: LSeg ((GoB f) * (i + 1),(j + 1)),((GoB f) * (i + 1),(j + 2)) c= L~ f and
A5: LSeg ((GoB f) * i,(j + 1)),((GoB f) * (i + 1),(j + 1)) c= L~ f ; :: thesis: contradiction
A6: i + 1 <= len (GoB f) by A1, NAT_1:13;
A7: 1 <= i + 1 by NAT_1:11;
A8: j < width (GoB f) by A2, NAT_1:13;
A9: 1 <= j + 1 by NAT_1:11;
j + (1 + 1) = (j + 1) + 1 ;
then A10: j + 2 <= width (GoB f) by A2, NAT_1:13;
j + 1 <= j + 2 by XREAL_1:8;
then A11: 1 <= j + 2 by A9, XXREAL_0:2;

per cases ( ( f /. 2 = (GoB f) * (i + 1),j & f /. 2 = (GoB f) * i,(j + 1) ) or ( f /. ((len f) -' 1) = (GoB f) * (i + 1),(j + 2) & f /. ((len f) -' 1) = (GoB f) * i,(j + 1) ) or ( f /. 2 = (GoB f) * (i + 1),(j + 2) & f /. 2 = (GoB f) * i,(j + 1) ) or ( f /. 2 = (GoB f) * (i + 1),(j + 2) & f /. 2 = (GoB f) * (i + 1),j ) or ( f /. 1 = (GoB f) * (i + 1),(j + 1) & ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),(j + 1) & ( ( f /. k = (GoB f) * i,(j + 1) & f /. (k + 2) = (GoB f) * (i + 1),j ) or ( f /. k = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * i,(j + 1) ) ) ) ) or ( ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),(j + 1) & ( ( f /. k = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * (i + 1),(j + 2) ) or ( f /. k = (GoB f) * (i + 1),(j + 2) & f /. (k + 2) = (GoB f) * (i + 1),j ) ) ) & f /. 1 = (GoB f) * (i + 1),(j + 1) ) or ( ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),(j + 1) & ( ( f /. k = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * (i + 1),(j + 2) ) or ( f /. k = (GoB f) * (i + 1),(j + 2) & f /. (k + 2) = (GoB f) * (i + 1),j ) ) ) & ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),(j + 1) & ( ( f /. k = (GoB f) * i,(j + 1) & f /. (k + 2) = (GoB f) * (i + 1),j ) or ( f /. k = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * i,(j + 1) ) ) ) ) ) by A1, A2, A3, A4, A5, A6, A7, Th55, Th57;

suppose A12: ( f /. 2 = (GoB f) * (i + 1),j & f /. 2 = (GoB f) * i,(j + 1) ) ; :: thesis: contradiction

( [(i + 1),j] in Indices (GoB f) & [i,(j + 1)] in Indices (GoB f) ) by A1, A2, A6, A7, A8, A9, MATRIX_1:37;
then i = i + 1 by A12, GOBOARD1:21;
hence contradiction ; :: thesis: verum

end;

suppose A13: ( f /. ((len f) -' 1) = (GoB f) * (i + 1),(j + 2) & f /. ((len f) -' 1) = (GoB f) * i,(j + 1) ) ; :: thesis: contradiction

( [(i + 1),(j + 2)] in Indices (GoB f) & [i,(j + 1)] in Indices (GoB f) ) by A1, A2, A6, A7, A9, A10, A11, MATRIX_1:37;
then i = i + 1 by A13, GOBOARD1:21;
hence contradiction ; :: thesis: verum

end;

suppose A14: ( f /. 2 = (GoB f) * (i + 1),(j + 2) & f /. 2 = (GoB f) * i,(j + 1) ) ; :: thesis: contradiction

( [(i + 1),(j + 2)] in Indices (GoB f) & [i,(j + 1)] in Indices (GoB f) ) by A1, A2, A6, A7, A9, A10, A11, MATRIX_1:37;
then i = i + 1 by A14, GOBOARD1:21;
hence contradiction ; :: thesis: verum

end;

suppose A15: ( f /. 2 = (GoB f) * (i + 1),(j + 2) & f /. 2 = (GoB f) * (i + 1),j ) ; :: thesis: contradiction

( [(i + 1),(j + 2)] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) ) by A2, A6, A7, A8, A10, A11, MATRIX_1:37;
then j = j + 2 by A15, GOBOARD1:21;
hence contradiction ; :: thesis: verum

end;

suppose that A16: f /. 1 = (GoB f) * (i + 1),(j + 1) and
A17: ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),(j + 1) & ( ( f /. k = (GoB f) * i,(j + 1) & f /. (k + 2) = (GoB f) * (i + 1),j ) or ( f /. k = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * i,(j + 1) ) ) ) ; :: thesis: contradiction

consider k being Element of NAT such that
A18: ( 1 <= k & k + 1 < len f ) and
A19: f /. (k + 1) = (GoB f) * (i + 1),(j + 1) and
( ( f /. k = (GoB f) * i,(j + 1) & f /. (k + 2) = (GoB f) * (i + 1),j ) or ( f /. k = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * i,(j + 1) ) ) by A17;
1 < k + 1 by A18, NAT_1:13;
hence contradiction by A16, A18, A19, Th38; :: thesis: verum

end;

suppose that A20: ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),(j + 1) & ( ( f /. k = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * (i + 1),(j + 2) ) or ( f /. k = (GoB f) * (i + 1),(j + 2) & f /. (k + 2) = (GoB f) * (i + 1),j ) ) ) and
A21: f /. 1 = (GoB f) * (i + 1),(j + 1) ; :: thesis: contradiction

consider k being Element of NAT such that
A22: ( 1 <= k & k + 1 < len f ) and
A23: f /. (k + 1) = (GoB f) * (i + 1),(j + 1) and
( ( f /. k = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * (i + 1),(j + 2) ) or ( f /. k = (GoB f) * (i + 1),(j + 2) & f /. (k + 2) = (GoB f) * (i + 1),j ) ) by A20;
1 < k + 1 by A22, NAT_1:13;
hence contradiction by A21, A22, A23, Th38; :: thesis: verum

end;

suppose that A24: ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),(j + 1) & ( ( f /. k = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * (i + 1),(j + 2) ) or ( f /. k = (GoB f) * (i + 1),(j + 2) & f /. (k + 2) = (GoB f) * (i + 1),j ) ) ) and
A25: ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),(j + 1) & ( ( f /. k = (GoB f) * i,(j + 1) & f /. (k + 2) = (GoB f) * (i + 1),j ) or ( f /. k = (GoB f) * (i + 1),j & f /. (k + 2) = (GoB f) * i,(j + 1) ) ) ) ; :: thesis: contradiction

consider k1 being Element of NAT such that
A26: ( 1 <= k1 & k1 + 1 < len f ) and
A27: f /. (k1 + 1) = (GoB f) * (i + 1),(j + 1) and
A28: ( ( f /. k1 = (GoB f) * (i + 1),j & f /. (k1 + 2) = (GoB f) * (i + 1),(j + 2) ) or ( f /. k1 = (GoB f) * (i + 1),(j + 2) & f /. (k1 + 2) = (GoB f) * (i + 1),j ) ) by A24;
consider k2 being Element of NAT such that
A29: ( 1 <= k2 & k2 + 1 < len f ) and
A30: f /. (k2 + 1) = (GoB f) * (i + 1),(j + 1) and
A31: ( ( f /. k2 = (GoB f) * i,(j + 1) & f /. (k2 + 2) = (GoB f) * (i + 1),j ) or ( f /. k2 = (GoB f) * (i + 1),j & f /. (k2 + 2) = (GoB f) * i,(j + 1) ) ) by A25;

A32: now

assume A33: k1 <> k2 ; :: thesis: contradiction

per cases ( k1 < k2 or k2 < k1 ) by A33, XXREAL_0:1;

suppose k1 < k2 ; :: thesis: contradiction

then ( k1 + 1 < k2 + 1 & 1 <= k1 + 1 ) by NAT_1:11, XREAL_1:8;
hence contradiction by A27, A29, A30, Th38; :: thesis: verum

end;

suppose k2 < k1 ; :: thesis: contradiction

then ( k2 + 1 < k1 + 1 & 1 <= k2 + 1 ) by NAT_1:11, XREAL_1:8;
hence contradiction by A26, A27, A30, Th38; :: thesis: verum

end;

end;

end;

now

per cases ( ( f /. k1 = (GoB f) * (i + 1),j & f /. k2 = (GoB f) * i,(j + 1) ) or ( f /. (k1 + 2) = (GoB f) * (i + 1),(j + 2) & f /. (k2 + 2) = (GoB f) * i,(j + 1) ) or ( f /. k1 = (GoB f) * (i + 1),(j + 2) & f /. k2 = (GoB f) * i,(j + 1) ) or ( f /. k1 = (GoB f) * (i + 1),(j + 2) & f /. k2 = (GoB f) * (i + 1),j ) ) by A28, A31;

suppose A34: ( f /. k1 = (GoB f) * (i + 1),j & f /. k2 = (GoB f) * i,(j + 1) ) ; :: thesis: contradiction

( [(i + 1),j] in Indices (GoB f) & [i,(j + 1)] in Indices (GoB f) ) by A1, A2, A6, A7, A8, A9, MATRIX_1:37;
then i = i + 1 by A32, A34, GOBOARD1:21;
hence contradiction ; :: thesis: verum

end;

suppose A35: ( f /. (k1 + 2) = (GoB f) * (i + 1),(j + 2) & f /. (k2 + 2) = (GoB f) * i,(j + 1) ) ; :: thesis: contradiction

( [(i + 1),(j + 2)] in Indices (GoB f) & [i,(j + 1)] in Indices (GoB f) ) by A1, A2, A6, A7, A9, A10, A11, MATRIX_1:37;
then i = i + 1 by A32, A35, GOBOARD1:21;
hence contradiction ; :: thesis: verum

end;

suppose A36: ( f /. k1 = (GoB f) * (i + 1),(j + 2) & f /. k2 = (GoB f) * i,(j + 1) ) ; :: thesis: contradiction

( [(i + 1),(j + 2)] in Indices (GoB f) & [i,(j + 1)] in Indices (GoB f) ) by A1, A2, A6, A7, A9, A10, A11, MATRIX_1:37;
then i = i + 1 by A32, A36, GOBOARD1:21;
hence contradiction ; :: thesis: verum

end;

suppose A37: ( f /. k1 = (GoB f) * (i + 1),(j + 2) & f /. k2 = (GoB f) * (i + 1),j ) ; :: thesis: contradiction

( [(i + 1),(j + 2)] in Indices (GoB f) & [(i + 1),j] in Indices (GoB f) ) by A2, A6, A7, A8, A10, A11, MATRIX_1:37;
then j = j + 2 by A32, A37, GOBOARD1:21;
hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;