:: JORDAN8 semantic presentation

begin


theorem :: JORDAN8:1
for D being set
for G being Matrix of D holds <*> D is_sequence_on G
proof
let D be set ; ::_thesis: for G being Matrix of D holds <*> D is_sequence_on G
let G be Matrix of D; ::_thesis: <*> D is_sequence_on G
set f = <*> D;
thus  ( ( for n being Element of NAT st n in dom (<*> D) holds
ex i, j being Element of NAT st
( [i,j] in Indices G & (<*> D) /. n = G * (i,j) ) ) & ( for n being Element of NAT st n in dom (<*> D) & n + 1 in dom (<*> D) holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & (<*> D) /. n = G * (m,k) & (<*> D) /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ) ) ; :: according to GOBOARD1:def_9 ::_thesis: verum
end;

theorem :: JORDAN8:2
for m being Element of NAT
for D being non empty set
for f being FinSequence of D
for G being Matrix of D st f is_sequence_on G holds
f /^ m is_sequence_on G
proof
let m be Element of NAT ; ::_thesis: for D being non empty set
for f being FinSequence of D
for G being Matrix of D st f is_sequence_on G holds
f /^ m is_sequence_on G
let D be non empty set ; ::_thesis: for f being FinSequence of D
for G being Matrix of D st f is_sequence_on G holds
f /^ m is_sequence_on G
let f be FinSequence of D; ::_thesis: for G being Matrix of D st f is_sequence_on G holds
f /^ m is_sequence_on G
let G be Matrix of D; ::_thesis: ( f is_sequence_on G implies f /^ m is_sequence_on G )
assume that
A1: for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * (i,j) ) and
A2: for n being Element of NAT st n in dom f & n + 1 in dom f holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & f /. n = G * (m,k) & f /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ; :: according to GOBOARD1:def_9 ::_thesis: f /^ m is_sequence_on G
set g = f /^ m;
hereby  :: according to GOBOARD1:def_9 ::_thesis: for b1 being Element of NAT holds
( not b1 in dom (f /^ m) or not b1 + 1 in dom (f /^ m) or for b2, b3, b4, b5 being Element of NAT holds
( not [b2,b3] in Indices G or not [b4,b5] in Indices G or not (f /^ m) /. b1 = G * (b2,b3) or not (f /^ m) /. (b1 + 1) = G * (b4,b5) or (abs (b2 - b4)) + (abs (b3 - b5)) = 1 ) )
let n be Element of NAT ; ::_thesis: ( n in dom (f /^ m) implies ex i, j being Element of NAT st
( [i,j] in Indices G & (f /^ m) /. n = G * (i,j) ) )
assume A3: n in dom (f /^ m) ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices G & (f /^ m) /. n = G * (i,j) )
then consider i, j being Element of NAT  such that
A4: [i,j] in Indices G and
A5: f /. (n + m) = G * (i,j) by A1, FINSEQ_5:26;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices G & (f /^ m) /. n = G * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices G & (f /^ m) /. n = G * (i,j) )
thus  [i,j] in Indices G by A4; ::_thesis: (f /^ m) /. n = G * (i,j)
thus  (f /^ m) /. n = G * (i,j) by A3, A5, FINSEQ_5:27; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: ( not n in dom (f /^ m) or not n + 1 in dom (f /^ m) or for b1, b2, b3, b4 being Element of NAT holds
( not [b1,b2] in Indices G or not [b3,b4] in Indices G or not (f /^ m) /. n = G * (b1,b2) or not (f /^ m) /. (n + 1) = G * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 ) )
assume that
A6: n in dom (f /^ m) and
A7: n + 1 in dom (f /^ m) ; ::_thesis: for b1, b2, b3, b4 being Element of NAT holds
( not [b1,b2] in Indices G or not [b3,b4] in Indices G or not (f /^ m) /. n = G * (b1,b2) or not (f /^ m) /. (n + 1) = G * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 )
let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( not [i1,j1] in Indices G or not [i2,j2] in Indices G or not (f /^ m) /. n = G * (i1,j1) or not (f /^ m) /. (n + 1) = G * (i2,j2) or (abs (i1 - i2)) + (abs (j1 - j2)) = 1 )
assume that
A8: [i1,j1] in Indices G and
A9: [i2,j2] in Indices G and
A10: (f /^ m) /. n = G * (i1,j1) and
A11: (f /^ m) /. (n + 1) = G * (i2,j2) ; ::_thesis: (abs (i1 - i2)) + (abs (j1 - j2)) = 1
A12: n + m in dom f by A6, FINSEQ_5:26;
A13: (n + 1) + m = (n + m) + 1 ;
then A14: (n + m) + 1 in dom f by A7, FINSEQ_5:26;
A15: f /. (n + m) = (f /^ m) /. n by A6, FINSEQ_5:27;
 f /. ((n + m) + 1) = (f /^ m) /. (n + 1) by A7, A13, FINSEQ_5:27;
hence  (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A2, A8, A9, A10, A11, A12, A14, A15; ::_thesis: verum
end;

theorem Th3: :: JORDAN8:3
for k being Element of NAT
for D being set
for f being FinSequence of D
for G being Matrix of D st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
ex i1, j1, i2, j2 being Element of NAT st
( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) )
proof
let k be Element of NAT ; ::_thesis: for D being set
for f being FinSequence of D
for G being Matrix of D st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
ex i1, j1, i2, j2 being Element of NAT st
( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) )
let D be set ; ::_thesis: for f being FinSequence of D
for G being Matrix of D st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
ex i1, j1, i2, j2 being Element of NAT st
( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) )
let f be FinSequence of D; ::_thesis: for G being Matrix of D st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
ex i1, j1, i2, j2 being Element of NAT st
( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) )
let G be Matrix of D; ::_thesis: ( 1 <= k & k + 1 <= len f & f is_sequence_on G implies ex i1, j1, i2, j2 being Element of NAT st
( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) ) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f and
A3: f is_sequence_on G ; ::_thesis: ex i1, j1, i2, j2 being Element of NAT st
( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) )
 k <= k + 1 by NAT_1:11;
then  k <= len f by A2, XXREAL_0:2;
then A4: k in dom f by A1, FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A5: [i1,j1] in Indices G and
A6: f /. k = G * (i1,j1) by A3, GOBOARD1:def_9;
 k + 1 >= 1 by NAT_1:11;
then A7: k + 1 in dom f by A2, FINSEQ_3:25;
then consider i2, j2 being Element of NAT  such that
A8: [i2,j2] in Indices G and
A9: f /. (k + 1) = G * (i2,j2) by A3, GOBOARD1:def_9;
A10: (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A4, A5, A6, A7, A8, A9, GOBOARD1:def_9;
now__::_thesis:_(_(_abs_(i1_-_i2)_=_1_&_j1_=_j2_&_(_i1_=_i2_+_1_or_i1_+_1_=_i2_)_&_j1_=_j2_)_or_(_i1_=_i2_&_abs_(j1_-_j2)_=_1_&_(_j1_=_j2_+_1_or_j1_+_1_=_j2_)_&_i1_=_i2_)_)
percases ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( i1 = i2 & abs (j1 - j2) = 1 ) ) by A10, SEQM_3:42;
casethat A11: abs (i1 - i2) = 1 and
A12: j1 = j2 ; ::_thesis: ( ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 )
 ( i1 - i2 = 1 or - (i1 - i2) = 1 ) by A11, ABSVALUE:def_1;
hence  ( i1 = i2 + 1 or i1 + 1 = i2 ) ; ::_thesis: j1 = j2
thus  j1 = j2 by A12; ::_thesis: verum
end;
casethat A13: i1 = i2 and
A14: abs (j1 - j2) = 1 ; ::_thesis: ( ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 )
 ( j1 - j2 = 1 or - (j1 - j2) = 1 ) by A14, ABSVALUE:def_1;
hence  ( j1 = j2 + 1 or j1 + 1 = j2 ) ; ::_thesis: i1 = i2
thus  i1 = i2 by A13; ::_thesis: verum
end;
end;
end;
hence  ex i1, j1, i2, j2 being Element of NAT st
( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) ) by A5, A6, A8, A9; ::_thesis: verum
end;


theorem :: JORDAN8:4
for G being Go-board
for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
( f is standard & f is special )
proof
let G be Go-board; ::_thesis: for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
( f is standard & f is special )
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G implies ( f is standard & f is special ) )
assume A1: f is_sequence_on G ; ::_thesis: ( f is standard & f is special )
thus  f is_sequence_on GoB f :: according to GOBOARD5:def_5 ::_thesis: f is special
proof
set F = GoB f;
thus  for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) by GOBOARD2:14; :: according to GOBOARD1:def_9 ::_thesis: for b1 being Element of NAT holds
( not b1 in dom f or not b1 + 1 in dom f or for b2, b3, b4, b5 being Element of NAT holds
( not [b2,b3] in Indices (GoB f) or not [b4,b5] in Indices (GoB f) or not f /. b1 = (GoB f) * (b2,b3) or not f /. (b1 + 1) = (GoB f) * (b4,b5) or (abs (b2 - b4)) + (abs (b3 - b5)) = 1 ) )
let n be Element of NAT ; ::_thesis: ( not n in dom f or not n + 1 in dom f or for b1, b2, b3, b4 being Element of NAT holds
( not [b1,b2] in Indices (GoB f) or not [b3,b4] in Indices (GoB f) or not f /. n = (GoB f) * (b1,b2) or not f /. (n + 1) = (GoB f) * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 ) )
assume that
A2: n in dom f and
A3: n + 1 in dom f ; ::_thesis: for b1, b2, b3, b4 being Element of NAT holds
( not [b1,b2] in Indices (GoB f) or not [b3,b4] in Indices (GoB f) or not f /. n = (GoB f) * (b1,b2) or not f /. (n + 1) = (GoB f) * (b3,b4) or (abs (b1 - b3)) + (abs (b2 - b4)) = 1 )
let m, k, i, j be Element of NAT ; ::_thesis: ( not [m,k] in Indices (GoB f) or not [i,j] in Indices (GoB f) or not f /. n = (GoB f) * (m,k) or not f /. (n + 1) = (GoB f) * (i,j) or (abs (m - i)) + (abs (k - j)) = 1 )
assume that
A4: [m,k] in Indices (GoB f) and
A5: [i,j] in Indices (GoB f) and
A6: f /. n = (GoB f) * (m,k) and
A7: f /. (n + 1) = (GoB f) * (i,j) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
A8: 1 <= m by A4, MATRIX_1:38;
A9: m <= len (GoB f) by A4, MATRIX_1:38;
A10: 1 <= k by A4, MATRIX_1:38;
A11: k <= width (GoB f) by A4, MATRIX_1:38;
A12: 1 <= i by A5, MATRIX_1:38;
A13: i <= len (GoB f) by A5, MATRIX_1:38;
A14: 1 <= j by A5, MATRIX_1:38;
A15: j <= width (GoB f) by A5, MATRIX_1:38;
then A16: ((GoB f) * (i,j)) `1 = ((GoB f) * (i,1)) `1 by A12, A13, A14, GOBOARD5:2;
A17: ((GoB f) * (i,k)) `1 = ((GoB f) * (i,1)) `1 by A10, A11, A12, A13, GOBOARD5:2;
A18: ((GoB f) * (i,j)) `2 = ((GoB f) * (1,j)) `2 by A12, A13, A14, A15, GOBOARD5:1;
A19: ((GoB f) * (m,j)) `2 = ((GoB f) * (1,j)) `2 by A8, A9, A14, A15, GOBOARD5:1;
A20: 1 <= n by A2, FINSEQ_3:25;
 n + 1 <= len f by A3, FINSEQ_3:25;
then consider i1, j1, i2, j2 being Element of NAT  such that
A21: [i1,j1] in Indices G and
A22: f /. n = G * (i1,j1) and
A23: [i2,j2] in Indices G and
A24: f /. (n + 1) = G * (i2,j2) and
A25: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A20, Th3;
A26: 1 <= i1 by A21, MATRIX_1:38;
A27: i1 <= len G by A21, MATRIX_1:38;
A28: 1 <= j1 by A21, MATRIX_1:38;
A29: j1 <= width G by A21, MATRIX_1:38;
A30: 1 <= i2 by A23, MATRIX_1:38;
A31: i2 <= len G by A23, MATRIX_1:38;
A32: 1 <= j2 by A23, MATRIX_1:38;
A33: j2 <= width G by A23, MATRIX_1:38;
A34: (G * (i1,j1)) `1 = (G * (i1,1)) `1 by A26, A27, A28, A29, GOBOARD5:2;
A35: (G * (i2,j2)) `1 = (G * (i2,1)) `1 by A30, A31, A32, A33, GOBOARD5:2;
A36: (G * (i1,j1)) `2 = (G * (1,j1)) `2 by A26, A27, A28, A29, GOBOARD5:1;
A37: (G * (i2,j1)) `2 = (G * (1,j1)) `2 by A28, A29, A30, A31, GOBOARD5:1;
A38: k + 1 >= 1 by NAT_1:12;
A39: j + 1 >= 1 by NAT_1:12;
A40: m + 1 >= 1 by NAT_1:12;
A41: i + 1 >= 1 by NAT_1:12;
A42: k + 1 > k by NAT_1:13;
A43: j + 1 > j by NAT_1:13;
A44: m + 1 > m by NAT_1:13;
A45: i + 1 > i by NAT_1:13;
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A25;
supposeA46: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
now__::_thesis:_not_m_<>_i
assume  m <> i ; ::_thesis: contradiction
then  ( m < i or m > i ) by XXREAL_0:1;
hence  contradiction by A6, A7, A8, A9, A10, A11, A12, A13, A16, A17, A22, A24, A34, A35, A46, GOBOARD5:3; ::_thesis: verum
end;
then A47: abs (m - i) = 0 by ABSVALUE:2;
now__::_thesis:_not_j_<=_k
assume  j <= k ; ::_thesis: contradiction
then A48: ((GoB f) * (i,j)) `2 <= ((GoB f) * (m,k)) `2 by A8, A9, A11, A14, A18, A19, SPRECT_3:12;
 j1 < j2 by A46, NAT_1:13;
hence  contradiction by A6, A7, A22, A24, A28, A30, A31, A33, A36, A37, A48, GOBOARD5:4; ::_thesis: verum
end;
then A49: k + 1 <= j by NAT_1:13;
now__::_thesis:_not_k_+_1_<_j
assume A50: k + 1 < j ; ::_thesis: contradiction
then A51: k + 1 < width (GoB f) by A15, XXREAL_0:2;
then consider l, i9 being Element of NAT  such that
A52: l in dom f and
A53: [i9,(k + 1)] in Indices (GoB f) and
A54: f /. l = (GoB f) * (i9,(k + 1)) by JORDAN5D:8, NAT_1:12;
A55: 1 <= i9 by A53, MATRIX_1:38;
 i9 <= len (GoB f) by A53, MATRIX_1:38;
then A56: ((GoB f) * (i9,(k + 1))) `2 = ((GoB f) * (1,(k + 1))) `2 by A38, A51, A55, GOBOARD5:1;
A57: ((GoB f) * (m,(k + 1))) `2 = ((GoB f) * (1,(k + 1))) `2 by A8, A9, A38, A51, GOBOARD5:1;
consider i19, j19 being Element of NAT  such that
A58: [i19,j19] in Indices G and
A59: f /. l = G * (i19,j19) by A1, A52, GOBOARD1:def_9;
A60: 1 <= i19 by A58, MATRIX_1:38;
A61: i19 <= len G by A58, MATRIX_1:38;
A62: 1 <= j19 by A58, MATRIX_1:38;
A63: j19 <= width G by A58, MATRIX_1:38;
A64: (G * (i19,j1)) `2 = (G * (1,j1)) `2 by A28, A29, A60, A61, GOBOARD5:1;
A65: (G * (i2,j2)) `2 = (G * (1,j2)) `2 by A30, A31, A32, A33, GOBOARD5:1;
A66: (G * (i19,j2)) `2 = (G * (1,j2)) `2 by A32, A33, A60, A61, GOBOARD5:1;
A67: now__::_thesis:_not_j1_>=_j19
assume  j1 >= j19 ; ::_thesis: contradiction
then  (G * (i19,j19)) `2 <= (G * (i1,j1)) `2 by A29, A36, A60, A61, A62, A64, SPRECT_3:12;
hence  contradiction by A6, A8, A9, A10, A22, A42, A51, A54, A56, A57, A59, GOBOARD5:4; ::_thesis: verum
end;
now__::_thesis:_not_j2_<=_j19
assume  j2 <= j19 ; ::_thesis: contradiction
then  (G * (i2,j2)) `2 <= (G * (i19,j19)) `2 by A32, A60, A61, A63, A65, A66, SPRECT_3:12;
hence  contradiction by A7, A8, A9, A15, A18, A19, A24, A38, A50, A54, A56, A57, A59, GOBOARD5:4; ::_thesis: verum
end;
hence  contradiction by A46, A67, NAT_1:13; ::_thesis: verum
end;
then  k + 1 = j by A49, XXREAL_0:1;
then  abs (j - k) = 1 by ABSVALUE:def_1;
hence  (abs (m - i)) + (abs (k - j)) = 1 by A47, UNIFORM1:11; ::_thesis: verum
end;
supposeA68: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
now__::_thesis:_not_k_<>_j
assume  k <> j ; ::_thesis: contradiction
then  ( k < j or k > j ) by XXREAL_0:1;
hence  contradiction by A6, A7, A8, A9, A10, A11, A14, A15, A18, A19, A22, A24, A36, A37, A68, GOBOARD5:4; ::_thesis: verum
end;
then A69: abs (k - j) = 0 by ABSVALUE:2;
now__::_thesis:_not_i_<=_m
assume  i <= m ; ::_thesis: contradiction
then A70: ((GoB f) * (i,j)) `1 <= ((GoB f) * (m,k)) `1 by A9, A10, A11, A12, A16, A17, SPRECT_3:13;
 i1 < i2 by A68, NAT_1:13;
hence  contradiction by A6, A7, A22, A24, A26, A28, A29, A31, A68, A70, GOBOARD5:3; ::_thesis: verum
end;
then A71: m + 1 <= i by NAT_1:13;
now__::_thesis:_not_m_+_1_<_i
assume A72: m + 1 < i ; ::_thesis: contradiction
then A73: m + 1 < len (GoB f) by A13, XXREAL_0:2;
then consider l, j9 being Element of NAT  such that
A74: l in dom f and
A75: [(m + 1),j9] in Indices (GoB f) and
A76: f /. l = (GoB f) * ((m + 1),j9) by JORDAN5D:7, NAT_1:12;
A77: 1 <= j9 by A75, MATRIX_1:38;
 j9 <= width (GoB f) by A75, MATRIX_1:38;
then A78: ((GoB f) * ((m + 1),j9)) `1 = ((GoB f) * ((m + 1),1)) `1 by A40, A73, A77, GOBOARD5:2;
A79: ((GoB f) * ((m + 1),k)) `1 = ((GoB f) * ((m + 1),1)) `1 by A10, A11, A40, A73, GOBOARD5:2;
consider i19, j19 being Element of NAT  such that
A80: [i19,j19] in Indices G and
A81: f /. l = G * (i19,j19) by A1, A74, GOBOARD1:def_9;
A82: 1 <= i19 by A80, MATRIX_1:38;
A83: i19 <= len G by A80, MATRIX_1:38;
A84: 1 <= j19 by A80, MATRIX_1:38;
A85: j19 <= width G by A80, MATRIX_1:38;
then A86: (G * (i1,j19)) `1 = (G * (i1,1)) `1 by A26, A27, A84, GOBOARD5:2;
A87: (G * (i2,j2)) `1 = (G * (i2,1)) `1 by A30, A31, A32, A33, GOBOARD5:2;
A88: (G * (i2,j19)) `1 = (G * (i2,1)) `1 by A30, A31, A84, A85, GOBOARD5:2;
A89: now__::_thesis:_not_i1_>=_i19
assume  i1 >= i19 ; ::_thesis: contradiction
then  (G * (i19,j19)) `1 <= (G * (i1,j1)) `1 by A27, A34, A82, A84, A85, A86, SPRECT_3:13;
hence  contradiction by A6, A8, A10, A11, A22, A44, A73, A76, A78, A79, A81, GOBOARD5:3; ::_thesis: verum
end;
now__::_thesis:_not_i2_<=_i19
assume  i2 <= i19 ; ::_thesis: contradiction
then  (G * (i2,j2)) `1 <= (G * (i19,j19)) `1 by A30, A83, A84, A85, A87, A88, SPRECT_3:13;
hence  contradiction by A7, A10, A11, A13, A16, A17, A24, A40, A72, A76, A78, A79, A81, GOBOARD5:3; ::_thesis: verum
end;
hence  contradiction by A68, A89, NAT_1:13; ::_thesis: verum
end;
then  m + 1 = i by A71, XXREAL_0:1;
then  abs (i - m) = 1 by ABSVALUE:def_1;
hence  (abs (m - i)) + (abs (k - j)) = 1 by A69, UNIFORM1:11; ::_thesis: verum
end;
supposeA90: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
now__::_thesis:_not_k_<>_j
assume  k <> j ; ::_thesis: contradiction
then  ( k < j or k > j ) by XXREAL_0:1;
hence  contradiction by A6, A7, A8, A9, A10, A11, A14, A15, A18, A19, A22, A24, A36, A37, A90, GOBOARD5:4; ::_thesis: verum
end;
then A91: abs (k - j) = 0 by ABSVALUE:2;
now__::_thesis:_not_m_<=_i
assume  m <= i ; ::_thesis: contradiction
then A92: ((GoB f) * (i,j)) `1 >= ((GoB f) * (m,k)) `1 by A8, A10, A11, A13, A16, A17, SPRECT_3:13;
 i1 > i2 by A90, NAT_1:13;
hence  contradiction by A6, A7, A22, A24, A27, A28, A29, A30, A90, A92, GOBOARD5:3; ::_thesis: verum
end;
then A93: i + 1 <= m by NAT_1:13;
now__::_thesis:_not_i_+_1_<_m
assume A94: i + 1 < m ; ::_thesis: contradiction
then A95: i + 1 < len (GoB f) by A9, XXREAL_0:2;
then consider l, j9 being Element of NAT  such that
A96: l in dom f and
A97: [(i + 1),j9] in Indices (GoB f) and
A98: f /. l = (GoB f) * ((i + 1),j9) by JORDAN5D:7, NAT_1:12;
A99: 1 <= j9 by A97, MATRIX_1:38;
 j9 <= width (GoB f) by A97, MATRIX_1:38;
then A100: ((GoB f) * ((i + 1),j9)) `1 = ((GoB f) * ((i + 1),1)) `1 by A41, A95, A99, GOBOARD5:2;
A101: ((GoB f) * ((i + 1),k)) `1 = ((GoB f) * ((i + 1),1)) `1 by A10, A11, A41, A95, GOBOARD5:2;
A102: ((GoB f) * ((i + 1),j)) `1 = ((GoB f) * ((i + 1),1)) `1 by A14, A15, A41, A95, GOBOARD5:2;
consider i19, j19 being Element of NAT  such that
A103: [i19,j19] in Indices G and
A104: f /. l = G * (i19,j19) by A1, A96, GOBOARD1:def_9;
A105: 1 <= i19 by A103, MATRIX_1:38;
A106: i19 <= len G by A103, MATRIX_1:38;
A107: 1 <= j19 by A103, MATRIX_1:38;
A108: j19 <= width G by A103, MATRIX_1:38;
then A109: (G * (i1,j19)) `1 = (G * (i1,1)) `1 by A26, A27, A107, GOBOARD5:2;
A110: (G * (i2,j2)) `1 = (G * (i2,1)) `1 by A30, A31, A32, A33, GOBOARD5:2;
A111: (G * (i2,j19)) `1 = (G * (i2,1)) `1 by A30, A31, A107, A108, GOBOARD5:2;
A112: now__::_thesis:_not_i2_>=_i19
assume  i2 >= i19 ; ::_thesis: contradiction
then  (G * (i19,j19)) `1 <= (G * (i2,j2)) `1 by A31, A105, A107, A108, A110, A111, SPRECT_3:13;
hence  contradiction by A7, A12, A14, A15, A24, A45, A95, A98, A100, A102, A104, GOBOARD5:3; ::_thesis: verum
end;
now__::_thesis:_not_i1_<=_i19
assume  i1 <= i19 ; ::_thesis: contradiction
then  (G * (i1,j1)) `1 <= (G * (i19,j19)) `1 by A26, A34, A106, A107, A108, A109, SPRECT_3:13;
hence  contradiction by A6, A9, A10, A11, A22, A41, A94, A98, A100, A101, A104, GOBOARD5:3; ::_thesis: verum
end;
hence  contradiction by A90, A112, NAT_1:13; ::_thesis: verum
end;
then  i + 1 = m by A93, XXREAL_0:1;
hence  (abs (m - i)) + (abs (k - j)) = 1 by A91, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA113: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: (abs (m - i)) + (abs (k - j)) = 1
now__::_thesis:_not_m_<>_i
assume  m <> i ; ::_thesis: contradiction
then  ( m < i or m > i ) by XXREAL_0:1;
hence  contradiction by A6, A7, A8, A9, A10, A11, A12, A13, A16, A17, A22, A24, A34, A35, A113, GOBOARD5:3; ::_thesis: verum
end;
then A114: abs (m - i) = 0 by ABSVALUE:2;
now__::_thesis:_not_j_>=_k
assume  j >= k ; ::_thesis: contradiction
then A115: ((GoB f) * (i,j)) `2 >= ((GoB f) * (m,k)) `2 by A8, A9, A10, A15, A18, A19, SPRECT_3:12;
 j1 > j2 by A113, NAT_1:13;
hence  contradiction by A6, A7, A22, A24, A29, A30, A31, A32, A36, A37, A115, GOBOARD5:4; ::_thesis: verum
end;
then A116: j + 1 <= k by NAT_1:13;
now__::_thesis:_not_j_+_1_<_k
assume A117: j + 1 < k ; ::_thesis: contradiction
then A118: j + 1 < width (GoB f) by A11, XXREAL_0:2;
then consider l, i9 being Element of NAT  such that
A119: l in dom f and
A120: [i9,(j + 1)] in Indices (GoB f) and
A121: f /. l = (GoB f) * (i9,(j + 1)) by JORDAN5D:8, NAT_1:12;
A122: 1 <= i9 by A120, MATRIX_1:38;
 i9 <= len (GoB f) by A120, MATRIX_1:38;
then A123: ((GoB f) * (i9,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2 by A39, A118, A122, GOBOARD5:1;
A124: ((GoB f) * (i,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2 by A12, A13, A39, A118, GOBOARD5:1;
A125: ((GoB f) * (m,(j + 1))) `2 = ((GoB f) * (1,(j + 1))) `2 by A8, A9, A39, A118, GOBOARD5:1;
consider i19, j19 being Element of NAT  such that
A126: [i19,j19] in Indices G and
A127: f /. l = G * (i19,j19) by A1, A119, GOBOARD1:def_9;
A128: 1 <= i19 by A126, MATRIX_1:38;
A129: i19 <= len G by A126, MATRIX_1:38;
A130: 1 <= j19 by A126, MATRIX_1:38;
A131: j19 <= width G by A126, MATRIX_1:38;
A132: (G * (i19,j1)) `2 = (G * (1,j1)) `2 by A28, A29, A128, A129, GOBOARD5:1;
A133: (G * (i2,j2)) `2 = (G * (1,j2)) `2 by A30, A31, A32, A33, GOBOARD5:1;
A134: (G * (i19,j2)) `2 = (G * (1,j2)) `2 by A32, A33, A128, A129, GOBOARD5:1;
A135: now__::_thesis:_not_j2_>=_j19
assume  j2 >= j19 ; ::_thesis: contradiction
then  (G * (i19,j19)) `2 <= (G * (i2,j2)) `2 by A33, A128, A129, A130, A133, A134, SPRECT_3:12;
hence  contradiction by A7, A12, A13, A14, A24, A43, A118, A121, A123, A124, A127, GOBOARD5:4; ::_thesis: verum
end;
now__::_thesis:_not_j1_<=_j19
assume  j1 <= j19 ; ::_thesis: contradiction
then  (G * (i1,j1)) `2 <= (G * (i19,j19)) `2 by A28, A36, A128, A129, A131, A132, SPRECT_3:12;
hence  contradiction by A6, A8, A9, A11, A22, A39, A117, A121, A123, A125, A127, GOBOARD5:4; ::_thesis: verum
end;
hence  contradiction by A113, A135, NAT_1:13; ::_thesis: verum
end;
then  j + 1 = k by A116, XXREAL_0:1;
hence  (abs (m - i)) + (abs (k - j)) = 1 by A114, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;
thus  f is special ::_thesis: verum
proof
let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
A136: i in NAT by ORDINAL1:def_12;
assume that
A137: 1 <= i and
A138: i + 1 <= len f ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 )
consider i1, j1, i2, j2 being Element of NAT  such that
A139: [i1,j1] in Indices G and
A140: f /. i = G * (i1,j1) and
A141: [i2,j2] in Indices G and
A142: f /. (i + 1) = G * (i2,j2) and
A143: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A136, A137, A138, Th3;
A144: 1 <= i1 by A139, MATRIX_1:38;
A145: i1 <= len G by A139, MATRIX_1:38;
A146: 1 <= j1 by A139, MATRIX_1:38;
A147: j1 <= width G by A139, MATRIX_1:38;
A148: 1 <= i2 by A141, MATRIX_1:38;
A149: i2 <= len G by A141, MATRIX_1:38;
A150: 1 <= j2 by A141, MATRIX_1:38;
A151: j2 <= width G by A141, MATRIX_1:38;
A152: (G * (i1,j1)) `2 = (G * (1,j1)) `2 by A144, A145, A146, A147, GOBOARD5:1;
 (G * (i1,j1)) `1 = (G * (i1,1)) `1 by A144, A145, A146, A147, GOBOARD5:2;
hence  ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A140, A142, A143, A148, A149, A150, A151, A152, GOBOARD5:1, GOBOARD5:2; ::_thesis: verum
end;
end;

theorem :: JORDAN8:5
for G being Go-board
for f being non empty FinSequence of (TOP-REAL 2) st len f >= 2 & f is_sequence_on G holds
not f is constant
proof
let G be Go-board; ::_thesis: for f being non empty FinSequence of (TOP-REAL 2) st len f >= 2 & f is_sequence_on G holds
not f is constant
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( len f >= 2 & f is_sequence_on G implies not f is constant )
assume that
A1: len f >= 2 and
A2: f is_sequence_on G ; ::_thesis: not f is constant
assume A3: for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m ; :: according to SEQM_3:def_10 ::_thesis: contradiction
 1 <= len f by A1, XXREAL_0:2;
then A4: 1 in dom f by FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A5: [i1,j1] in Indices G and
A6: f /. 1 = G * (i1,j1) by A2, GOBOARD1:def_9;
A7: 1 + 1 in dom f by A1, FINSEQ_3:25;
then consider i2, j2 being Element of NAT  such that
A8: [i2,j2] in Indices G and
A9: f /. 2 = G * (i2,j2) by A2, GOBOARD1:def_9;
A10: f /. 1 = f . 1 by A4, PARTFUN1:def_6
.= f . 2 by A3, A4, A7
.= f /. 2 by A7, PARTFUN1:def_6 ;
then A11: i1 = i2 by A5, A6, A8, A9, GOBOARD1:5;
A12: j1 = j2 by A5, A6, A8, A9, A10, GOBOARD1:5;
A13: abs (i1 - i2) = 0 by A11, ABSVALUE:2;
 (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A2, A4, A5, A6, A7, A8, A9, GOBOARD1:def_9;
hence  contradiction by A12, A13; ::_thesis: verum
end;

theorem :: JORDAN8:6
for G being Go-board
for p being Point of (TOP-REAL 2)
for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Element of NAT st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds
f ^ <*p*> is_sequence_on G
proof
let G be Go-board; ::_thesis: for p being Point of (TOP-REAL 2)
for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Element of NAT st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds
f ^ <*p*> is_sequence_on G
let p be Point of (TOP-REAL 2); ::_thesis: for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Element of NAT st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds
f ^ <*p*> is_sequence_on G
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G & ex i, j being Element of NAT st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) implies f ^ <*p*> is_sequence_on G )
assume that
A1: f is_sequence_on G and
A2: ex i, j being Element of NAT st
( [i,j] in Indices G & p = G * (i,j) ) and
A3: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ; ::_thesis: f ^ <*p*> is_sequence_on G
A4: for n being Element of NAT st n in dom f & n + 1 in dom f holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & f /. n = G * (m,k) & f /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A1, GOBOARD1:def_9;
A5: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_<*p*>_&_n_+_1_in_dom_<*p*>_holds_
for_m,_k,_i,_j_being_Element_of_NAT_st_[m,k]_in_Indices_G_&_[i,j]_in_Indices_G_&_<*p*>_/._n_=_G_*_(m,k)_&_<*p*>_/._(n_+_1)_=_G_*_(i,j)_holds_
(abs_(m_-_i))_+_(abs_(k_-_j))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom <*p*> & n + 1 in dom <*p*> implies for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & <*p*> /. n = G * (m,k) & <*p*> /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 )
assume that
A6: n in dom <*p*> and
A7: n + 1 in dom <*p*> ; ::_thesis: for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & <*p*> /. n = G * (m,k) & <*p*> /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1
A8: 1 <= n by A6, FINSEQ_3:25;
A9: n + 1 <= len <*p*> by A7, FINSEQ_3:25;
A10: 1 + 1 <= n + 1 by A8, XREAL_1:6;
 n + 1 <= 1 by A9, FINSEQ_1:39;
hence  for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & <*p*> /. n = G * (m,k) & <*p*> /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A10, XXREAL_0:2; ::_thesis: verum
end;
now__::_thesis:_for_m,_k,_i,_j_being_Element_of_NAT_st_[m,k]_in_Indices_G_&_[i,j]_in_Indices_G_&_f_/._(len_f)_=_G_*_(m,k)_&_<*p*>_/._1_=_G_*_(i,j)_&_len_f_in_dom_f_&_1_in_dom_<*p*>_holds_
1_=_(abs_(m_-_i))_+_(abs_(k_-_j))
let m, k, i, j be Element of NAT ; ::_thesis: ( [m,k] in Indices G & [i,j] in Indices G & f /. (len f) = G * (m,k) & <*p*> /. 1 = G * (i,j) & len f in dom f & 1 in dom <*p*> implies 1 = (abs (m - i)) + (abs (k - j)) )
assume that
A11: [m,k] in Indices G and
A12: [i,j] in Indices G and
A13: f /. (len f) = G * (m,k) and
A14: <*p*> /. 1 = G * (i,j) and
 len f in dom f and
 1 in dom <*p*> ; ::_thesis: 1 = (abs (m - i)) + (abs (k - j))
 <*p*> /. 1 = p by FINSEQ_4:16;
then  (abs (i - m)) + (abs (j - k)) = 1 by A3, A11, A12, A13, A14;
hence 1 = (abs (m - i)) + (abs (j - k)) by UNIFORM1:11
.= (abs (m - i)) + (abs (k - j)) by UNIFORM1:11 ;
::_thesis: verum
end;
then A15: for n being Element of NAT st n in dom (f ^ <*p*>) & n + 1 in dom (f ^ <*p*>) holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & (f ^ <*p*>) /. n = G * (m,k) & (f ^ <*p*>) /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A4, A5, GOBOARD1:24;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(f_^_<*p*>)_holds_
ex_i,_j_being_Element_of_NAT_st_
(_[i,j]_in_Indices_G_&_(f_^_<*p*>)_/._n_=_G_*_(i,j)_)
let n be Element of NAT ; ::_thesis: ( n in dom (f ^ <*p*>) implies ex i, j being Element of NAT st
( [j,b3] in Indices G & (f ^ <*p*>) /. i = G * (j,b3) ) )
assume A16: n in dom (f ^ <*p*>) ; ::_thesis: ex i, j being Element of NAT st
( [j,b3] in Indices G & (f ^ <*p*>) /. i = G * (j,b3) )
percases ( n in dom f or ex l being Nat st
( l in dom <*p*> & n = (len f) + l ) ) by A16, FINSEQ_1:25;
supposeA17: n in dom f ; ::_thesis: ex i, j being Element of NAT st
( [j,b3] in Indices G & (f ^ <*p*>) /. i = G * (j,b3) )
then consider i, j being Element of NAT  such that
A18: [i,j] in Indices G and
A19: f /. n = G * (i,j) by A1, GOBOARD1:def_9;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )
thus  [i,j] in Indices G by A18; ::_thesis: (f ^ <*p*>) /. n = G * (i,j)
thus  (f ^ <*p*>) /. n = G * (i,j) by A17, A19, FINSEQ_4:68; ::_thesis: verum
end;
suppose ex l being Nat st
( l in dom <*p*> & n = (len f) + l ) ; ::_thesis: ex i, j being Element of NAT st
( [j,b3] in Indices G & (f ^ <*p*>) /. i = G * (j,b3) )
then consider l being Nat such that
A20: l in dom <*p*> and
A21: n = (len f) + l ;
consider i, j being Element of NAT  such that
A22: [i,j] in Indices G and
A23: p = G * (i,j) by A2;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices G & (f ^ <*p*>) /. n = G * (i,j) )
thus  [i,j] in Indices G by A22; ::_thesis: (f ^ <*p*>) /. n = G * (i,j)
A24: l <= len <*p*> by A20, FINSEQ_3:25;
A25: 1 <= l by A20, FINSEQ_3:25;
 l <= 1 by A24, FINSEQ_1:39;
then  l = 1 by A25, XXREAL_0:1;
then  <*p*> /. l = p by FINSEQ_4:16;
hence  (f ^ <*p*>) /. n = G * (i,j) by A20, A21, A23, FINSEQ_4:69; ::_thesis: verum
end;
end;
end;
hence  f ^ <*p*> is_sequence_on G by A15, GOBOARD1:def_9; ::_thesis: verum
end;

theorem :: JORDAN8:7
for i, k, j being Element of NAT
for G being Go-board st i + k < len G & 1 <= j & j < width G & cell (G,i,j) meets cell (G,(i + k),j) holds
k <= 1
proof
let i, k, j be Element of NAT ; ::_thesis: for G being Go-board st i + k < len G & 1 <= j & j < width G & cell (G,i,j) meets cell (G,(i + k),j) holds
k <= 1
let G be Go-board; ::_thesis: ( i + k < len G & 1 <= j & j < width G & cell (G,i,j) meets cell (G,(i + k),j) implies k <= 1 )
assume that
A1: i + k < len G and
A2: 1 <= j and
A3: j < width G and
A4: cell (G,i,j) meets cell (G,(i + k),j) and
A5: k > 1 ; ::_thesis: contradiction
 (cell (G,i,j)) /\ (cell (G,(i + k),j)) <> {} by A4, XBOOLE_0:def_7;
then consider p being Point of (TOP-REAL 2) such that
A6: p in (cell (G,i,j)) /\ (cell (G,(i + k),j)) by SUBSET_1:4;
A7: p in cell (G,i,j) by A6, XBOOLE_0:def_4;
A8: p in cell (G,(i + k),j) by A6, XBOOLE_0:def_4;
 i + k >= 1 by A5, NAT_1:12;
then  cell (G,(i + k),j) =  {  |[r9,s9]| where r9, s9 is Real : ( (G * ((i + k),1)) `1 <= r9 & r9 <= (G * (((i + k) + 1),1)) `1 & (G * (1,j)) `2 <= s9 & s9 <= (G * (1,(j + 1))) `2 )  }  by A1, A2, A3, GOBRD11:32;
then consider r9, s9 being Real such that
A9: p = |[r9,s9]| and
A10: (G * ((i + k),1)) `1 <= r9 and
 r9 <= (G * (((i + k) + 1),1)) `1 and
 (G * (1,j)) `2 <= s9 and
 s9 <= (G * (1,(j + 1))) `2 by A8;
A11: 1 < width G by A2, A3, XXREAL_0:2;
 ( i = 0 or i > 0 ) by NAT_1:3;
then A12: ( i = 0 or i >= 1 + 0 ) by NAT_1:9;
percases ( i = 0 or i >= 1 ) by A12;
supposeA13: i = 0 ; ::_thesis: contradiction
then  cell (G,i,j) =  {  |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 )  }  by A2, A3, GOBRD11:26;
then consider r, s being Real such that
A14: p = |[r,s]| and
A15: r <= (G * (1,1)) `1 and
 (G * (1,j)) `2 <= s and
 s <= (G * (1,(j + 1))) `2 by A7;
A16: k <= len G by A1, NAT_1:12;
A17: p `1 = r by A14, EUCLID:52;
 p `1 = r9 by A9, EUCLID:52;
then  (G * (k,1)) `1 <= (G * (1,1)) `1 by A10, A13, A15, A17, XXREAL_0:2;
hence  contradiction by A5, A11, A16, GOBOARD5:3; ::_thesis: verum
end;
supposeA18: i >= 1 ; ::_thesis: contradiction
 i < len G by A1, NAT_1:12;
then  cell (G,i,j) =  {  |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 )  }  by A2, A3, A18, GOBRD11:32;
then consider r, s being Real such that
A19: p = |[r,s]| and
 (G * (i,1)) `1 <= r and
A20: r <= (G * ((i + 1),1)) `1 and
 (G * (1,j)) `2 <= s and
 s <= (G * (1,(j + 1))) `2 by A7;
A21: 1 <= i + 1 by NAT_1:12;
A22: i + 1 < k + i by A5, XREAL_1:6;
A23: p `1 = r by A19, EUCLID:52;
 p `1 = r9 by A9, EUCLID:52;
then  (G * ((i + k),1)) `1 <= (G * ((i + 1),1)) `1 by A10, A20, A23, XXREAL_0:2;
hence  contradiction by A1, A11, A21, A22, GOBOARD5:3; ::_thesis: verum
end;
end;
end;

theorem Th8: :: JORDAN8:8
for C being non empty compact Subset of (TOP-REAL 2) holds
( C is vertical iff E-bound C <= W-bound C )
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( C is vertical iff E-bound C <= W-bound C )
A1: E-bound C >= W-bound C by SPRECT_1:21;
 ( C is vertical iff W-bound C = E-bound C ) by SPRECT_1:15;
hence  ( C is vertical iff E-bound C <= W-bound C ) by A1, XXREAL_0:1; ::_thesis: verum
end;

theorem Th9: :: JORDAN8:9
for C being non empty compact Subset of (TOP-REAL 2) holds
( C is horizontal iff N-bound C <= S-bound C )
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( C is horizontal iff N-bound C <= S-bound C )
A1: N-bound C >= S-bound C by SPRECT_1:22;
 ( C is horizontal iff N-bound C = S-bound C ) by SPRECT_1:16;
hence  ( C is horizontal iff N-bound C <= S-bound C ) by A1, XXREAL_0:1; ::_thesis: verum
end;

definition
let C be Subset of (TOP-REAL 2);
let n be Nat;
deffunc H1( Nat, Nat) ->  Element of the carrier of (TOP-REAL 2) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ($1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ($2 - 2)))]|;
A1: (2 |^ n) + 3 > 0 by NAT_1:3;
func Gauge (C,n) ->  Matrix of (TOP-REAL 2) means :Def1: :: JORDAN8:def 1
( len it = (2 |^ n) + 3 & len it = width it & ( for i, j being Nat st [i,j] in Indices it holds
it * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) );
existence
 ex b1 being Matrix of (TOP-REAL 2) st
( len b1 = (2 |^ n) + 3 & len b1 = width b1 & ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) )
proof
consider M being Matrix of (2 |^ n) + 3,(2 |^ n) + 3, the carrier of (TOP-REAL 2) such that
A2: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H1(i,j) from MATRIX_1:sch_1();
take  M ; ::_thesis: ( len M = (2 |^ n) + 3 & len M = width M & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) )
thus  len M = (2 |^ n) + 3 by MATRIX_1:def_2; ::_thesis: ( len M = width M & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) )
hence  len M = width M by A1, MATRIX_1:23; ::_thesis: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]|
thus  for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Matrix of (TOP-REAL 2) st len b1 = (2 |^ n) + 3 & len b1 = width b1 & ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) & len b2 = (2 |^ n) + 3 & len b2 = width b2 & ( for i, j being Nat st [i,j] in Indices b2 holds
b2 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) holds
b1 = b2
proof
let M1, M2 be Matrix of (TOP-REAL 2); ::_thesis: ( len M1 = (2 |^ n) + 3 & len M1 = width M1 & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) & len M2 = (2 |^ n) + 3 & len M2 = width M2 & ( for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) implies M1 = M2 )
assume that
A3: len M1 = (2 |^ n) + 3 and
A4: len M1 = width M1 and
A5: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = H1(i,j) and
A6: len M2 = (2 |^ n) + 3 and
A7: len M2 = width M2 and
A8: for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) = H1(i,j) ; ::_thesis: M1 = M2
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M1_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A9: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
A10: M1 is Matrix of (2 |^ n) + 3,(2 |^ n) + 3, the carrier of (TOP-REAL 2) by A1, A3, A4, MATRIX_1:20;
 M2 is Matrix of (2 |^ n) + 3,(2 |^ n) + 3, the carrier of (TOP-REAL 2) by A1, A6, A7, MATRIX_1:20;
then A11: [i,j] in Indices M2 by A9, A10, MATRIX_1:26;
thus M1 * (i,j) = H1(i,j) by A5, A9
.= M2 * (i,j) by A8, A11 ; ::_thesis: verum
end;
hence  M1 = M2 by A3, A4, A6, A7, MATRIX_1:21; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Gauge JORDAN8:def_1_:_
 for C being Subset of (TOP-REAL 2)
for n being Nat
for b3 being Matrix of (TOP-REAL 2) holds
( b3 = Gauge (C,n) iff ( len b3 = (2 |^ n) + 3 & len b3 = width b3 & ( for i, j being Nat st [i,j] in Indices b3 holds
b3 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) ) );

registration
let C be non empty Subset of (TOP-REAL 2);
let n be Nat;
cluster Gauge (C,n) -> V3() X_equal-in-line Y_equal-in-column ;
coherence
 ( not Gauge (C,n) is empty-yielding & Gauge (C,n) is X_equal-in-line & Gauge (C,n) is Y_equal-in-column )
proof
set M = Gauge (C,n);
A1: len (Gauge (C,n)) = (2 |^ n) + 3 by Def1;
 len (Gauge (C,n)) = width (Gauge (C,n)) by Def1;
hence  Gauge (C,n) is V3() by A1, GOBOARD1:def_3; ::_thesis: ( Gauge (C,n) is X_equal-in-line & Gauge (C,n) is Y_equal-in-column )
A2: Indices (Gauge (C,n)) = [:(dom (Gauge (C,n))),(Seg (width (Gauge (C,n)))):] by MATRIX_1:def_4;
thus  Gauge (C,n) is X_equal-in-line ::_thesis: Gauge (C,n) is Y_equal-in-column
proof
let i be Element of NAT ; :: according to GOBOARD1:def_4 ::_thesis: ( not i in dom (Gauge (C,n)) or X_axis (Line ((Gauge (C,n)),i)) is constant )
assume A3: i in dom (Gauge (C,n)) ; ::_thesis: X_axis (Line ((Gauge (C,n)),i)) is constant
set l = Line ((Gauge (C,n)),i);
set f = X_axis (Line ((Gauge (C,n)),i));
let j1 be Element of NAT ; :: according to SEQM_3:def_10 ::_thesis: for b1 being Element of NAT holds
( not j1 in dom (X_axis (Line ((Gauge (C,n)),i))) or not b1 in dom (X_axis (Line ((Gauge (C,n)),i))) or (X_axis (Line ((Gauge (C,n)),i))) . j1 = (X_axis (Line ((Gauge (C,n)),i))) . b1 )
let j2 be Element of NAT ; ::_thesis: ( not j1 in dom (X_axis (Line ((Gauge (C,n)),i))) or not j2 in dom (X_axis (Line ((Gauge (C,n)),i))) or (X_axis (Line ((Gauge (C,n)),i))) . j1 = (X_axis (Line ((Gauge (C,n)),i))) . j2 )
assume that
A4: j1 in dom (X_axis (Line ((Gauge (C,n)),i))) and
A5: j2 in dom (X_axis (Line ((Gauge (C,n)),i))) ; ::_thesis: (X_axis (Line ((Gauge (C,n)),i))) . j1 = (X_axis (Line ((Gauge (C,n)),i))) . j2
 len (Line ((Gauge (C,n)),i)) = width (Gauge (C,n)) by MATRIX_1:def_7;
then A6: dom (Line ((Gauge (C,n)),i)) = Seg (width (Gauge (C,n))) by FINSEQ_1:def_3;
A7: dom (X_axis (Line ((Gauge (C,n)),i))) = dom (Line ((Gauge (C,n)),i)) by SPRECT_2:15;
then A8: (Line ((Gauge (C,n)),i)) /. j1 = (Line ((Gauge (C,n)),i)) . j1 by A4, PARTFUN1:def_6
.= (Gauge (C,n)) * (i,j1) by A4, A6, A7, MATRIX_1:def_7 ;
A9: [i,j1] in Indices (Gauge (C,n)) by A2, A3, A4, A6, A7, ZFMISC_1:87;
A10: (Line ((Gauge (C,n)),i)) /. j2 = (Line ((Gauge (C,n)),i)) . j2 by A5, A7, PARTFUN1:def_6
.= (Gauge (C,n)) * (i,j2) by A5, A6, A7, MATRIX_1:def_7 ;
A11: [i,j2] in Indices (Gauge (C,n)) by A2, A3, A5, A6, A7, ZFMISC_1:87;
set x = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2));
set d = ((N-bound C) - (S-bound C)) / (2 |^ n);
thus (X_axis (Line ((Gauge (C,n)),i))) . j1 = ((Line ((Gauge (C,n)),i)) /. j1) `1 by A4, GOBOARD1:def_1
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j1 - 2)))]| `1 by A8, A9, Def1
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2)) by EUCLID:52
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j2 - 2)))]| `1 by EUCLID:52
.= ((Line ((Gauge (C,n)),i)) /. j2) `1 by A10, A11, Def1
.= (X_axis (Line ((Gauge (C,n)),i))) . j2 by A5, GOBOARD1:def_1 ; ::_thesis: verum
end;
thus  Gauge (C,n) is Y_equal-in-column ::_thesis: verum
proof
let j be Element of NAT ; :: according to GOBOARD1:def_5 ::_thesis: ( not j in Seg (width (Gauge (C,n))) or Y_axis (Col ((Gauge (C,n)),j)) is constant )
assume A12: j in Seg (width (Gauge (C,n))) ; ::_thesis: Y_axis (Col ((Gauge (C,n)),j)) is constant
set c = Col ((Gauge (C,n)),j);
set f = Y_axis (Col ((Gauge (C,n)),j));
let i1 be Element of NAT ; :: according to SEQM_3:def_10 ::_thesis: for b1 being Element of NAT holds
( not i1 in dom (Y_axis (Col ((Gauge (C,n)),j))) or not b1 in dom (Y_axis (Col ((Gauge (C,n)),j))) or (Y_axis (Col ((Gauge (C,n)),j))) . i1 = (Y_axis (Col ((Gauge (C,n)),j))) . b1 )
let i2 be Element of NAT ; ::_thesis: ( not i1 in dom (Y_axis (Col ((Gauge (C,n)),j))) or not i2 in dom (Y_axis (Col ((Gauge (C,n)),j))) or (Y_axis (Col ((Gauge (C,n)),j))) . i1 = (Y_axis (Col ((Gauge (C,n)),j))) . i2 )
assume that
A13: i1 in dom (Y_axis (Col ((Gauge (C,n)),j))) and
A14: i2 in dom (Y_axis (Col ((Gauge (C,n)),j))) ; ::_thesis: (Y_axis (Col ((Gauge (C,n)),j))) . i1 = (Y_axis (Col ((Gauge (C,n)),j))) . i2
 len (Col ((Gauge (C,n)),j)) = len (Gauge (C,n)) by MATRIX_1:def_8;
then A15: dom (Col ((Gauge (C,n)),j)) = dom (Gauge (C,n)) by FINSEQ_3:29;
A16: dom (Y_axis (Col ((Gauge (C,n)),j))) = dom (Col ((Gauge (C,n)),j)) by SPRECT_2:16;
then A17: (Col ((Gauge (C,n)),j)) /. i1 = (Col ((Gauge (C,n)),j)) . i1 by A13, PARTFUN1:def_6
.= (Gauge (C,n)) * (i1,j) by A13, A15, A16, MATRIX_1:def_8 ;
A18: [i1,j] in Indices (Gauge (C,n)) by A2, A12, A13, A15, A16, ZFMISC_1:87;
A19: (Col ((Gauge (C,n)),j)) /. i2 = (Col ((Gauge (C,n)),j)) . i2 by A14, A16, PARTFUN1:def_6
.= (Gauge (C,n)) * (i2,j) by A14, A15, A16, MATRIX_1:def_8 ;
A20: [i2,j] in Indices (Gauge (C,n)) by A2, A12, A14, A15, A16, ZFMISC_1:87;
set y = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2));
set d = ((E-bound C) - (W-bound C)) / (2 |^ n);
thus (Y_axis (Col ((Gauge (C,n)),j))) . i1 = ((Col ((Gauge (C,n)),j)) /. i1) `2 by A13, GOBOARD1:def_2
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| `2 by A17, A18, Def1
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)) by EUCLID:52
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| `2 by EUCLID:52
.= ((Col ((Gauge (C,n)),j)) /. i2) `2 by A19, A20, Def1
.= (Y_axis (Col ((Gauge (C,n)),j))) . i2 by A14, GOBOARD1:def_2 ; ::_thesis: verum
end;
end;
end;

registration
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
cluster Gauge (C,n) ->  Y_increasing-in-line X_increasing-in-column ;
coherence
 ( Gauge (C,n) is Y_increasing-in-line & Gauge (C,n) is X_increasing-in-column )
proof
set M = Gauge (C,n);
A1: Indices (Gauge (C,n)) = [:(dom (Gauge (C,n))),(Seg (width (Gauge (C,n)))):] by MATRIX_1:def_4;
thus  Gauge (C,n) is Y_increasing-in-line ::_thesis: Gauge (C,n) is X_increasing-in-column
proof
let i be Element of NAT ; :: according to GOBOARD1:def_6 ::_thesis: ( not i in dom (Gauge (C,n)) or not Y_axis (Line ((Gauge (C,n)),i)) is V79() )
assume A2: i in dom (Gauge (C,n)) ; ::_thesis: Y_axis (Line ((Gauge (C,n)),i)) is V79()
set l = Line ((Gauge (C,n)),i);
set f = Y_axis (Line ((Gauge (C,n)),i));
let j1, j2 be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: ( not j1 in K64((Y_axis (Line ((Gauge (C,n)),i)))) or not j2 in K64((Y_axis (Line ((Gauge (C,n)),i)))) or j2 <= j1 or not K412((Y_axis (Line ((Gauge (C,n)),i))),j2) <= K412((Y_axis (Line ((Gauge (C,n)),i))),j1) )
assume that
A3: j1 in dom (Y_axis (Line ((Gauge (C,n)),i))) and
A4: j2 in dom (Y_axis (Line ((Gauge (C,n)),i))) and
A5: j1 < j2 ; ::_thesis: not K412((Y_axis (Line ((Gauge (C,n)),i))),j2) <= K412((Y_axis (Line ((Gauge (C,n)),i))),j1)
 len (Line ((Gauge (C,n)),i)) = width (Gauge (C,n)) by MATRIX_1:def_7;
then A6: dom (Line ((Gauge (C,n)),i)) = Seg (width (Gauge (C,n))) by FINSEQ_1:def_3;
A7: dom (Y_axis (Line ((Gauge (C,n)),i))) = dom (Line ((Gauge (C,n)),i)) by SPRECT_2:16;
then A8: (Line ((Gauge (C,n)),i)) /. j1 = (Line ((Gauge (C,n)),i)) . j1 by A3, PARTFUN1:def_6
.= (Gauge (C,n)) * (i,j1) by A3, A6, A7, MATRIX_1:def_7 ;
A9: [i,j1] in Indices (Gauge (C,n)) by A1, A2, A3, A6, A7, ZFMISC_1:87;
A10: (Line ((Gauge (C,n)),i)) /. j2 = (Line ((Gauge (C,n)),i)) . j2 by A4, A7, PARTFUN1:def_6
.= (Gauge (C,n)) * (i,j2) by A4, A6, A7, MATRIX_1:def_7 ;
A11: [i,j2] in Indices (Gauge (C,n)) by A1, A2, A4, A6, A7, ZFMISC_1:87;
set x = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2));
set d = ((N-bound C) - (S-bound C)) / (2 |^ n);
A12: (Y_axis (Line ((Gauge (C,n)),i))) . j1 = ((Line ((Gauge (C,n)),i)) /. j1) `2 by A3, GOBOARD1:def_2
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j1 - 2)))]| `2 by A8, A9, Def1
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j1 - 2)) by EUCLID:52 ;
A13: (Y_axis (Line ((Gauge (C,n)),i))) . j2 = ((Line ((Gauge (C,n)),i)) /. j2) `2 by A4, GOBOARD1:def_2
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j2 - 2)))]| `2 by A10, A11, Def1
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j2 - 2)) by EUCLID:52 ;
 N-bound C > S-bound C by Th9;
then A14: (N-bound C) - (S-bound C) > 0 by XREAL_1:50;
 2 |^ n > 0 by NEWTON:83;
then A15: ((N-bound C) - (S-bound C)) / (2 |^ n) > 0 by A14, XREAL_1:139;
 j1 - 2 < j2 - 2 by A5, XREAL_1:9;
then  (((N-bound C) - (S-bound C)) / (2 |^ n)) * (j1 - 2) < (((N-bound C) - (S-bound C)) / (2 |^ n)) * (j2 - 2) by A15, XREAL_1:68;
hence  (Y_axis (Line ((Gauge (C,n)),i))) . j1 < (Y_axis (Line ((Gauge (C,n)),i))) . j2 by A12, A13, XREAL_1:8; ::_thesis: verum
end;
let j be Element of NAT ; :: according to GOBOARD1:def_7 ::_thesis: ( not j in Seg (width (Gauge (C,n))) or not X_axis (Col ((Gauge (C,n)),j)) is V79() )
assume A16: j in Seg (width (Gauge (C,n))) ; ::_thesis: X_axis (Col ((Gauge (C,n)),j)) is V79()
set c = Col ((Gauge (C,n)),j);
set f = X_axis (Col ((Gauge (C,n)),j));
let i1 be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: for b1 being Element of NAT holds
( not i1 in K64((X_axis (Col ((Gauge (C,n)),j)))) or not b1 in K64((X_axis (Col ((Gauge (C,n)),j)))) or b1 <= i1 or not K412((X_axis (Col ((Gauge (C,n)),j))),b1) <= K412((X_axis (Col ((Gauge (C,n)),j))),i1) )
let i2 be Element of NAT ; ::_thesis: ( not i1 in K64((X_axis (Col ((Gauge (C,n)),j)))) or not i2 in K64((X_axis (Col ((Gauge (C,n)),j)))) or i2 <= i1 or not K412((X_axis (Col ((Gauge (C,n)),j))),i2) <= K412((X_axis (Col ((Gauge (C,n)),j))),i1) )
assume that
A17: i1 in dom (X_axis (Col ((Gauge (C,n)),j))) and
A18: i2 in dom (X_axis (Col ((Gauge (C,n)),j))) and
A19: i1 < i2 ; ::_thesis: not K412((X_axis (Col ((Gauge (C,n)),j))),i2) <= K412((X_axis (Col ((Gauge (C,n)),j))),i1)
 len (Col ((Gauge (C,n)),j)) = len (Gauge (C,n)) by MATRIX_1:def_8;
then A20: dom (Col ((Gauge (C,n)),j)) = dom (Gauge (C,n)) by FINSEQ_3:29;
A21: dom (X_axis (Col ((Gauge (C,n)),j))) = dom (Col ((Gauge (C,n)),j)) by SPRECT_2:15;
then A22: (Col ((Gauge (C,n)),j)) /. i1 = (Col ((Gauge (C,n)),j)) . i1 by A17, PARTFUN1:def_6
.= (Gauge (C,n)) * (i1,j) by A17, A20, A21, MATRIX_1:def_8 ;
A23: [i1,j] in Indices (Gauge (C,n)) by A1, A16, A17, A20, A21, ZFMISC_1:87;
A24: (Col ((Gauge (C,n)),j)) /. i2 = (Col ((Gauge (C,n)),j)) . i2 by A18, A21, PARTFUN1:def_6
.= (Gauge (C,n)) * (i2,j) by A18, A20, A21, MATRIX_1:def_8 ;
A25: [i2,j] in Indices (Gauge (C,n)) by A1, A16, A18, A20, A21, ZFMISC_1:87;
set y = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2));
set d = ((E-bound C) - (W-bound C)) / (2 |^ n);
A26: (X_axis (Col ((Gauge (C,n)),j))) . i1 = ((Col ((Gauge (C,n)),j)) /. i1) `1 by A17, GOBOARD1:def_1
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| `1 by A22, A23, Def1
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2)) by EUCLID:52 ;
A27: (X_axis (Col ((Gauge (C,n)),j))) . i2 = ((Col ((Gauge (C,n)),j)) /. i2) `1 by A18, GOBOARD1:def_1
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| `1 by A24, A25, Def1
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2)) by EUCLID:52 ;
 E-bound C > W-bound C by Th8;
then A28: (E-bound C) - (W-bound C) > 0 by XREAL_1:50;
 2 |^ n > 0 by NEWTON:83;
then A29: ((E-bound C) - (W-bound C)) / (2 |^ n) > 0 by A28, XREAL_1:139;
 i1 - 2 < i2 - 2 by A19, XREAL_1:9;
then  (((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2) < (((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2) by A29, XREAL_1:68;
hence  (X_axis (Col ((Gauge (C,n)),j))) . i1 < (X_axis (Col ((Gauge (C,n)),j))) . i2 by A26, A27, XREAL_1:8; ::_thesis: verum
end;
end;

theorem Th10: :: JORDAN8:10
for T being non empty Subset of (TOP-REAL 2)
for n being Nat holds len (Gauge (T,n)) >= 4
proof
let T be non empty Subset of (TOP-REAL 2); ::_thesis: for n being Nat holds len (Gauge (T,n)) >= 4
let n be Nat; ::_thesis: len (Gauge (T,n)) >= 4
set G = Gauge (T,n);
A1: len (Gauge (T,n)) = (2 |^ n) + 3 by Def1;
 2 |^ n >= n + 1 by NEWTON:85;
then A2: len (Gauge (T,n)) >= (n + 1) + 3 by A1, XREAL_1:6;
 n + 4 >= 4 by NAT_1:12;
hence  len (Gauge (T,n)) >= 4 by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem :: JORDAN8:11
for j, n being Element of NAT
for T being non empty Subset of (TOP-REAL 2) st 1 <= j & j <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (2,j)) `1 = W-bound T
proof
let j, n be Element of NAT ; ::_thesis: for T being non empty Subset of (TOP-REAL 2) st 1 <= j & j <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (2,j)) `1 = W-bound T
let T be non empty Subset of (TOP-REAL 2); ::_thesis: ( 1 <= j & j <= len (Gauge (T,n)) implies ((Gauge (T,n)) * (2,j)) `1 = W-bound T )
set G = Gauge (T,n);
set W = W-bound T;
set S = S-bound T;
set E = E-bound T;
set N = N-bound T;
assume that
A1: 1 <= j and
A2: j <= len (Gauge (T,n)) ; ::_thesis: ((Gauge (T,n)) * (2,j)) `1 = W-bound T
A3: len (Gauge (T,n)) = width (Gauge (T,n)) by Def1;
 len (Gauge (T,n)) >= 4 by Th10;
then  2 <= len (Gauge (T,n)) by XXREAL_0:2;
then  [2,j] in Indices (Gauge (T,n)) by A1, A2, A3, MATRIX_1:36;
then  (Gauge (T,n)) * (2,j) = |[((W-bound T) + ((((E-bound T) - (W-bound T)) / (2 |^ n)) * (2 - 2))),((S-bound T) + ((((N-bound T) - (S-bound T)) / (2 |^ n)) * (j - 2)))]| by Def1;
hence  ((Gauge (T,n)) * (2,j)) `1 = W-bound T by EUCLID:52; ::_thesis: verum
end;

theorem :: JORDAN8:12
for j, n being Element of NAT
for T being non empty Subset of (TOP-REAL 2) st 1 <= j & j <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j)) `1 = E-bound T
proof
let j, n be Element of NAT ; ::_thesis: for T being non empty Subset of (TOP-REAL 2) st 1 <= j & j <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j)) `1 = E-bound T
let T be non empty Subset of (TOP-REAL 2); ::_thesis: ( 1 <= j & j <= len (Gauge (T,n)) implies ((Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j)) `1 = E-bound T )
set G = Gauge (T,n);
set W = W-bound T;
set S = S-bound T;
set E = E-bound T;
set N = N-bound T;
assume that
A1: 1 <= j and
A2: j <= len (Gauge (T,n)) ; ::_thesis: ((Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j)) `1 = E-bound T
A3: len (Gauge (T,n)) = (2 |^ n) + 3 by Def1;
A4: len (Gauge (T,n)) = width (Gauge (T,n)) by Def1;
A5: len (Gauge (T,n)) >= 4 by Th10;
then  1 < len (Gauge (T,n)) by XXREAL_0:2;
then A6: 1 <= (len (Gauge (T,n))) -' 1 by NAT_D:49;
A7: ((len (Gauge (T,n))) -' 1) - 2 = ((len (Gauge (T,n))) - 1) - 2 by A5, XREAL_1:233, XXREAL_0:2
.= 2 |^ n by A3 ;
A8: 2 |^ n > 0 by NEWTON:83;
 (len (Gauge (T,n))) -' 1 <= len (Gauge (T,n)) by NAT_D:35;
then  [((len (Gauge (T,n))) -' 1),j] in Indices (Gauge (T,n)) by A1, A2, A4, A6, MATRIX_1:36;
then  (Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j) = |[((W-bound T) + ((((E-bound T) - (W-bound T)) / (2 |^ n)) * (((len (Gauge (T,n))) -' 1) - 2))),((S-bound T) + ((((N-bound T) - (S-bound T)) / (2 |^ n)) * (j - 2)))]| by Def1;
hence ((Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j)) `1 = (W-bound T) + ((((E-bound T) - (W-bound T)) / (2 |^ n)) * (2 |^ n)) by A7, EUCLID:52
.= (W-bound T) + ((E-bound T) - (W-bound T)) by A8, XCMPLX_1:87
.= E-bound T ;
::_thesis: verum
end;

theorem :: JORDAN8:13
for i, n being Element of NAT
for T being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (i,2)) `2 = S-bound T
proof
let i, n be Element of NAT ; ::_thesis: for T being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (i,2)) `2 = S-bound T
let T be non empty Subset of (TOP-REAL 2); ::_thesis: ( 1 <= i & i <= len (Gauge (T,n)) implies ((Gauge (T,n)) * (i,2)) `2 = S-bound T )
set G = Gauge (T,n);
set W = W-bound T;
set S = S-bound T;
set E = E-bound T;
set N = N-bound T;
assume that
A1: 1 <= i and
A2: i <= len (Gauge (T,n)) ; ::_thesis: ((Gauge (T,n)) * (i,2)) `2 = S-bound T
A3: len (Gauge (T,n)) = width (Gauge (T,n)) by Def1;
 len (Gauge (T,n)) >= 4 by Th10;
then  2 <= len (Gauge (T,n)) by XXREAL_0:2;
then  [i,2] in Indices (Gauge (T,n)) by A1, A2, A3, MATRIX_1:36;
then  (Gauge (T,n)) * (i,2) = |[((W-bound T) + ((((E-bound T) - (W-bound T)) / (2 |^ n)) * (i - 2))),((S-bound T) + ((((N-bound T) - (S-bound T)) / (2 |^ n)) * (2 - 2)))]| by Def1;
hence  ((Gauge (T,n)) * (i,2)) `2 = S-bound T by EUCLID:52; ::_thesis: verum
end;

theorem :: JORDAN8:14
for i, n being Element of NAT
for T being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (i,((len (Gauge (T,n))) -' 1))) `2 = N-bound T
proof
let i, n be Element of NAT ; ::_thesis: for T being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (i,((len (Gauge (T,n))) -' 1))) `2 = N-bound T
let T be non empty Subset of (TOP-REAL 2); ::_thesis: ( 1 <= i & i <= len (Gauge (T,n)) implies ((Gauge (T,n)) * (i,((len (Gauge (T,n))) -' 1))) `2 = N-bound T )
set G = Gauge (T,n);
set W = W-bound T;
set S = S-bound T;
set E = E-bound T;
set N = N-bound T;
assume that
A1: 1 <= i and
A2: i <= len (Gauge (T,n)) ; ::_thesis: ((Gauge (T,n)) * (i,((len (Gauge (T,n))) -' 1))) `2 = N-bound T
A3: len (Gauge (T,n)) = (2 |^ n) + 3 by Def1;
A4: len (Gauge (T,n)) = width (Gauge (T,n)) by Def1;
A5: len (Gauge (T,n)) >= 4 by Th10;
then  1 < len (Gauge (T,n)) by XXREAL_0:2;
then A6: 1 <= (len (Gauge (T,n))) -' 1 by NAT_D:49;
A7: ((len (Gauge (T,n))) -' 1) - 2 = ((len (Gauge (T,n))) - 1) - 2 by A5, XREAL_1:233, XXREAL_0:2
.= 2 |^ n by A3 ;
A8: 2 |^ n > 0 by NEWTON:83;
 (len (Gauge (T,n))) -' 1 <= len (Gauge (T,n)) by NAT_D:35;
then  [i,((len (Gauge (T,n))) -' 1)] in Indices (Gauge (T,n)) by A1, A2, A4, A6, MATRIX_1:36;
then  (Gauge (T,n)) * (i,((len (Gauge (T,n))) -' 1)) = |[((W-bound T) + ((((E-bound T) - (W-bound T)) / (2 |^ n)) * (i - 2))),((S-bound T) + ((((N-bound T) - (S-bound T)) / (2 |^ n)) * (((len (Gauge (T,n))) -' 1) - 2)))]| by Def1;
hence ((Gauge (T,n)) * (i,((len (Gauge (T,n))) -' 1))) `2 = (S-bound T) + ((((N-bound T) - (S-bound T)) / (2 |^ n)) * (2 |^ n)) by A7, EUCLID:52
.= (S-bound T) + ((N-bound T) - (S-bound T)) by A8, XCMPLX_1:87
.= N-bound T ;
::_thesis: verum
end;


theorem :: JORDAN8:15
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n being Nat st i <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) misses C
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for i, n being Nat st i <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) misses C
let i, n be Nat; ::_thesis: ( i <= len (Gauge (C,n)) implies cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) misses C )
set G = Gauge (C,n);
A1: i in NAT by ORDINAL1:def_12;
assume A2: i <= len (Gauge (C,n)) ; ::_thesis: cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) misses C
A3: len (Gauge (C,n)) = (2 |^ n) + (1 + 2) by Def1;
A4: len (Gauge (C,n)) = width (Gauge (C,n)) by Def1;
assume  (cell ((Gauge (C,n)),i,(len (Gauge (C,n))))) /\ C <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider p being Point of (TOP-REAL 2) such that
A5: p in (cell ((Gauge (C,n)),i,(len (Gauge (C,n))))) /\ C by SUBSET_1:4;
A6: p in cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) by A5, XBOOLE_0:def_4;
A7: p in C by A5, XBOOLE_0:def_4;
 4 <= len (Gauge (C,n)) by Th10;
then A8: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
set W = W-bound C;
set S = S-bound C;
set E = E-bound C;
set N = N-bound C;
set NS = ((N-bound C) - (S-bound C)) / (2 |^ n);
 [1,(width (Gauge (C,n)))] in Indices (Gauge (C,n)) by A4, A8, MATRIX_1:36;
then A9: (Gauge (C,n)) * (1,(width (Gauge (C,n)))) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((width (Gauge (C,n))) - 2)))]| by Def1;
A10: 2 |^ n > 0 by NEWTON:83;
 N-bound C > S-bound C by Th9;
then A11: (N-bound C) - (S-bound C) > 0 by XREAL_1:50;
(((N-bound C) - (S-bound C)) / (2 |^ n)) * ((width (Gauge (C,n))) - 2) = ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (2 |^ n)) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * 1) by A3, A4
.= ((N-bound C) - (S-bound C)) + (((N-bound C) - (S-bound C)) / (2 |^ n)) by A10, XCMPLX_1:87 ;
then  ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) by A9, EUCLID:52;
then A12: ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 > N-bound C by A10, A11, XREAL_1:29, XREAL_1:139;
 ( i = 0 or i > 0 ) by NAT_1:3;
then A13: ( i = 0 or i >= 1 + 0 ) by NAT_1:9;
percases ( i = 0 or i = len (Gauge (C,n)) or ( 1 <= i & i < len (Gauge (C,n)) ) ) by A2, A13, XXREAL_0:1;
suppose i = 0 ; ::_thesis: contradiction
then  cell ((Gauge (C,n)),i,(width (Gauge (C,n)))) =  {  |[r,s]| where r, s is Real : ( r <= ((Gauge (C,n)) * (1,1)) `1 & ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s )  }  by GOBRD11:25;
then consider r, s being Real such that
A14: p = |[r,s]| and
 r <= ((Gauge (C,n)) * (1,1)) `1 and
A15: ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s by A4, A6;
 p `2 = s by A14, EUCLID:52;
then  N-bound C < p `2 by A12, A15, XXREAL_0:2;
hence  contradiction by A7, PSCOMP_1:24; ::_thesis: verum
end;
suppose i = len (Gauge (C,n)) ; ::_thesis: contradiction
then  cell ((Gauge (C,n)),i,(width (Gauge (C,n)))) =  {  |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r & ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s )  }  by GOBRD11:28;
then consider r, s being Real such that
A16: p = |[r,s]| and
 ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r and
A17: ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s by A4, A6;
 p `2 = s by A16, EUCLID:52;
then  N-bound C < p `2 by A12, A17, XXREAL_0:2;
hence  contradiction by A7, PSCOMP_1:24; ::_thesis: verum
end;
suppose ( 1 <= i & i < len (Gauge (C,n)) ) ; ::_thesis: contradiction
then  cell ((Gauge (C,n)),i,(width (Gauge (C,n)))) =  {  |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i + 1),1)) `1 & ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s )  }  by A1, GOBRD11:31;
then consider r, s being Real such that
A18: p = |[r,s]| and
 ((Gauge (C,n)) * (i,1)) `1 <= r and
 r <= ((Gauge (C,n)) * ((i + 1),1)) `1 and
A19: ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s by A4, A6;
 p `2 = s by A18, EUCLID:52;
then  N-bound C < p `2 by A12, A19, XXREAL_0:2;
hence  contradiction by A7, PSCOMP_1:24; ::_thesis: verum
end;
end;
end;

theorem :: JORDAN8:16
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n being Nat st j <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),(len (Gauge (C,n))),j) misses C
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for j, n being Nat st j <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),(len (Gauge (C,n))),j) misses C
let j, n be Nat; ::_thesis: ( j <= len (Gauge (C,n)) implies cell ((Gauge (C,n)),(len (Gauge (C,n))),j) misses C )
set G = Gauge (C,n);
A1: j in NAT by ORDINAL1:def_12;
assume A2: j <= len (Gauge (C,n)) ; ::_thesis: cell ((Gauge (C,n)),(len (Gauge (C,n))),j) misses C
A3: len (Gauge (C,n)) = (2 |^ n) + (1 + 2) by Def1;
A4: len (Gauge (C,n)) = width (Gauge (C,n)) by Def1;
assume  (cell ((Gauge (C,n)),(len (Gauge (C,n))),j)) /\ C <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider p being Point of (TOP-REAL 2) such that
A5: p in (cell ((Gauge (C,n)),(len (Gauge (C,n))),j)) /\ C by SUBSET_1:4;
A6: p in cell ((Gauge (C,n)),(len (Gauge (C,n))),j) by A5, XBOOLE_0:def_4;
A7: p in C by A5, XBOOLE_0:def_4;
 4 <= len (Gauge (C,n)) by Th10;
then A8: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
set W = W-bound C;
set S = S-bound C;
set E = E-bound C;
set N = N-bound C;
set EW = ((E-bound C) - (W-bound C)) / (2 |^ n);
 [(len (Gauge (C,n))),1] in Indices (Gauge (C,n)) by A4, A8, MATRIX_1:36;
then A9: (Gauge (C,n)) * ((len (Gauge (C,n))),1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)))]| by Def1;
A10: 2 |^ n > 0 by NEWTON:83;
 E-bound C > W-bound C by Th8;
then A11: (E-bound C) - (W-bound C) > 0 by XREAL_1:50;
(((E-bound C) - (W-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2) = ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (2 |^ n)) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * 1) by A3
.= ((E-bound C) - (W-bound C)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A10, XCMPLX_1:87 ;
then  ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 = (E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A9, EUCLID:52;
then A12: ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 > E-bound C by A10, A11, XREAL_1:29, XREAL_1:139;
 ( j = 0 or j > 0 ) by NAT_1:3;
then A13: ( j = 0 or j >= 1 + 0 ) by NAT_1:9;
percases ( j = 0 or j = len (Gauge (C,n)) or ( 1 <= j & j < len (Gauge (C,n)) ) ) by A2, A13, XXREAL_0:1;
suppose j = 0 ; ::_thesis: contradiction
then  cell ((Gauge (C,n)),(len (Gauge (C,n))),j) =  {  |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r & s <= ((Gauge (C,n)) * (1,1)) `2 )  }  by GOBRD11:27;
then consider r, s being Real such that
A14: p = |[r,s]| and
A15: ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r and
 s <= ((Gauge (C,n)) * (1,1)) `2 by A6;
 p `1 = r by A14, EUCLID:52;
then  E-bound C < p `1 by A12, A15, XXREAL_0:2;
hence  contradiction by A7, PSCOMP_1:24; ::_thesis: verum
end;
suppose j = len (Gauge (C,n)) ; ::_thesis: contradiction
then  cell ((Gauge (C,n)),(len (Gauge (C,n))),j) =  {  |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r & ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s )  }  by A4, GOBRD11:28;
then consider r, s being Real such that
A16: p = |[r,s]| and
A17: ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r and
 ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s by A6;
 p `1 = r by A16, EUCLID:52;
then  E-bound C < p `1 by A12, A17, XXREAL_0:2;
hence  contradiction by A7, PSCOMP_1:24; ::_thesis: verum
end;
suppose ( 1 <= j & j < len (Gauge (C,n)) ) ; ::_thesis: contradiction
then  cell ((Gauge (C,n)),(len (Gauge (C,n))),j) =  {  |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r & ((Gauge (C,n)) * (1,j)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j + 1))) `2 )  }  by A1, A4, GOBRD11:29;
then consider r, s being Real such that
A18: p = |[r,s]| and
A19: ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r and
 ((Gauge (C,n)) * (1,j)) `2 <= s and
 s <= ((Gauge (C,n)) * (1,(j + 1))) `2 by A6;
 p `1 = r by A18, EUCLID:52;
then  E-bound C < p `1 by A12, A19, XXREAL_0:2;
hence  contradiction by A7, PSCOMP_1:24; ::_thesis: verum
end;
end;
end;

theorem :: JORDAN8:17
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n being Nat st i <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),i,0) misses C
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for i, n being Nat st i <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),i,0) misses C
let i, n be Nat; ::_thesis: ( i <= len (Gauge (C,n)) implies cell ((Gauge (C,n)),i,0) misses C )
set G = Gauge (C,n);
A1: i in NAT by ORDINAL1:def_12;
assume A2: i <= len (Gauge (C,n)) ; ::_thesis: cell ((Gauge (C,n)),i,0) misses C
A3: len (Gauge (C,n)) = width (Gauge (C,n)) by Def1;
assume  (cell ((Gauge (C,n)),i,0)) /\ C <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider p being Point of (TOP-REAL 2) such that
A4: p in (cell ((Gauge (C,n)),i,0)) /\ C by SUBSET_1:4;
A5: p in cell ((Gauge (C,n)),i,0) by A4, XBOOLE_0:def_4;
A6: p in C by A4, XBOOLE_0:def_4;
 4 <= len (Gauge (C,n)) by Th10;
then A7: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
set W = W-bound C;
set S = S-bound C;
set E = E-bound C;
set N = N-bound C;
set NS = ((N-bound C) - (S-bound C)) / (2 |^ n);
 [1,1] in Indices (Gauge (C,n)) by A3, A7, MATRIX_1:36;
then  (Gauge (C,n)) * (1,1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)))]| by Def1;
then A8: ((Gauge (C,n)) * (1,1)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (- 1)) by EUCLID:52;
A9: 2 |^ n > 0 by NEWTON:83;
 N-bound C > S-bound C by Th9;
then  (N-bound C) - (S-bound C) > 0 by XREAL_1:50;
then  ((N-bound C) - (S-bound C)) / (2 |^ n) > 0 by A9, XREAL_1:139;
then  (((N-bound C) - (S-bound C)) / (2 |^ n)) * (- 1) < 0 * (- 1) by XREAL_1:69;
then A10: ((Gauge (C,n)) * (1,1)) `2 < (S-bound C) + 0 by A8, XREAL_1:6;
 ( i = 0 or i > 0 ) by NAT_1:3;
then A11: ( i = 0 or i >= 1 + 0 ) by NAT_1:9;
percases ( i = 0 or i = len (Gauge (C,n)) or ( 1 <= i & i < len (Gauge (C,n)) ) ) by A2, A11, XXREAL_0:1;
suppose i = 0 ; ::_thesis: contradiction
then  cell ((Gauge (C,n)),i,0) =  {  |[r,s]| where r, s is Real : ( r <= ((Gauge (C,n)) * (1,1)) `1 & s <= ((Gauge (C,n)) * (1,1)) `2 )  }  by GOBRD11:24;
then consider r, s being Real such that
A12: p = |[r,s]| and
 r <= ((Gauge (C,n)) * (1,1)) `1 and
A13: s <= ((Gauge (C,n)) * (1,1)) `2 by A5;
 p `2 = s by A12, EUCLID:52;
then  S-bound C > p `2 by A10, A13, XXREAL_0:2;
hence  contradiction by A6, PSCOMP_1:24; ::_thesis: verum
end;
suppose i = len (Gauge (C,n)) ; ::_thesis: contradiction
then  cell ((Gauge (C,n)),i,0) =  {  |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r & s <= ((Gauge (C,n)) * (1,1)) `2 )  }  by GOBRD11:27;
then consider r, s being Real such that
A14: p = |[r,s]| and
 ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r and
A15: s <= ((Gauge (C,n)) * (1,1)) `2 by A5;
 p `2 = s by A14, EUCLID:52;
then  S-bound C > p `2 by A10, A15, XXREAL_0:2;
hence  contradiction by A6, PSCOMP_1:24; ::_thesis: verum
end;
suppose ( 1 <= i & i < len (Gauge (C,n)) ) ; ::_thesis: contradiction
then  cell ((Gauge (C,n)),i,0) =  {  |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i + 1),1)) `1 & s <= ((Gauge (C,n)) * (1,1)) `2 )  }  by A1, GOBRD11:30;
then consider r, s being Real such that
A16: p = |[r,s]| and
 ((Gauge (C,n)) * (i,1)) `1 <= r and
 r <= ((Gauge (C,n)) * ((i + 1),1)) `1 and
A17: s <= ((Gauge (C,n)) * (1,1)) `2 by A5;
 p `2 = s by A16, EUCLID:52;
then  S-bound C > p `2 by A10, A17, XXREAL_0:2;
hence  contradiction by A6, PSCOMP_1:24; ::_thesis: verum
end;
end;
end;

theorem :: JORDAN8:18
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n being Nat st j <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),0,j) misses C
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for j, n being Nat st j <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),0,j) misses C
let j, n be Nat; ::_thesis: ( j <= len (Gauge (C,n)) implies cell ((Gauge (C,n)),0,j) misses C )
set G = Gauge (C,n);
A1: j in NAT by ORDINAL1:def_12;
assume A2: j <= len (Gauge (C,n)) ; ::_thesis: cell ((Gauge (C,n)),0,j) misses C
A3: len (Gauge (C,n)) = width (Gauge (C,n)) by Def1;
assume  (cell ((Gauge (C,n)),0,j)) /\ C <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider p being Point of (TOP-REAL 2) such that
A4: p in (cell ((Gauge (C,n)),0,j)) /\ C by SUBSET_1:4;
A5: p in cell ((Gauge (C,n)),0,j) by A4, XBOOLE_0:def_4;
A6: p in C by A4, XBOOLE_0:def_4;
 4 <= len (Gauge (C,n)) by Th10;
then A7: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
set W = W-bound C;
set S = S-bound C;
set E = E-bound C;
set N = N-bound C;
set EW = ((E-bound C) - (W-bound C)) / (2 |^ n);
 [1,1] in Indices (Gauge (C,n)) by A3, A7, MATRIX_1:36;
then  (Gauge (C,n)) * (1,1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)))]| by Def1;
then A8: ((Gauge (C,n)) * (1,1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (- 1)) by EUCLID:52;
A9: 2 |^ n > 0 by NEWTON:83;
 E-bound C > W-bound C by Th8;
then  (E-bound C) - (W-bound C) > 0 by XREAL_1:50;
then  ((E-bound C) - (W-bound C)) / (2 |^ n) > 0 by A9, XREAL_1:139;
then  (((E-bound C) - (W-bound C)) / (2 |^ n)) * (- 1) < 0 * (- 1) by XREAL_1:69;
then A10: ((Gauge (C,n)) * (1,1)) `1 < (W-bound C) + 0 by A8, XREAL_1:6;
 ( j = 0 or j > 0 ) by NAT_1:3;
then A11: ( j = 0 or j >= 1 + 0 ) by NAT_1:9;
percases ( j = 0 or j = len (Gauge (C,n)) or ( 1 <= j & j < len (Gauge (C,n)) ) ) by A2, A11, XXREAL_0:1;
suppose j = 0 ; ::_thesis: contradiction
then  cell ((Gauge (C,n)),0,j) =  {  |[r,s]| where r, s is Real : ( r <= ((Gauge (C,n)) * (1,1)) `1 & s <= ((Gauge (C,n)) * (1,1)) `2 )  }  by GOBRD11:24;
then consider r, s being Real such that
A12: p = |[r,s]| and
A13: r <= ((Gauge (C,n)) * (1,1)) `1 and
 s <= ((Gauge (C,n)) * (1,1)) `2 by A5;
 p `1 = r by A12, EUCLID:52;
then  W-bound C > p `1 by A10, A13, XXREAL_0:2;
hence  contradiction by A6, PSCOMP_1:24; ::_thesis: verum
end;
suppose j = len (Gauge (C,n)) ; ::_thesis: contradiction
then  cell ((Gauge (C,n)),0,j) =  {  |[r,s]| where r, s is Real : ( r <= ((Gauge (C,n)) * (1,1)) `1 & ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s )  }  by A3, GOBRD11:25;
then consider r, s being Real such that
A14: p = |[r,s]| and
A15: r <= ((Gauge (C,n)) * (1,1)) `1 and
 ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s by A5;
 p `1 = r by A14, EUCLID:52;
then  W-bound C > p `1 by A10, A15, XXREAL_0:2;
hence  contradiction by A6, PSCOMP_1:24; ::_thesis: verum
end;
suppose ( 1 <= j & j < len (Gauge (C,n)) ) ; ::_thesis: contradiction
then  cell ((Gauge (C,n)),0,j) =  {  |[r,s]| where r, s is Real : ( r <= ((Gauge (C,n)) * (1,1)) `1 & ((Gauge (C,n)) * (1,j)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j + 1))) `2 )  }  by A1, A3, GOBRD11:26;
then consider r, s being Real such that
A16: p = |[r,s]| and
A17: r <= ((Gauge (C,n)) * (1,1)) `1 and
 ((Gauge (C,n)) * (1,j)) `2 <= s and
 s <= ((Gauge (C,n)) * (1,(j + 1))) `2 by A5;
 p `1 = r by A16, EUCLID:52;
then  W-bound C > p `1 by A10, A17, XXREAL_0:2;
hence  contradiction by A6, PSCOMP_1:24; ::_thesis: verum
end;
end;
end;