:: JORDAN1I semantic presentation begin theorem Th1: :: JORDAN1I:1 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 A1: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32; then 1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69; then 1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:70, XXREAL_0:2; then 1 < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:71, XXREAL_0:2; then 1 < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:72, XXREAL_0:2; then 1 < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:73, XXREAL_0:2; hence (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A1, SPRECT_2:74, XXREAL_0:2; ::_thesis: verum end; theorem Th2: :: JORDAN1I:2 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 A1: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32; then 1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69; hence (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A1, SPRECT_2:70, XXREAL_0:2; ::_thesis: verum end; theorem Th3: :: JORDAN1I:3 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 A1: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32; then 1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69; then 1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:70, XXREAL_0:2; then 1 < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:71, XXREAL_0:2; hence (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A1, SPRECT_2:72, XXREAL_0:2; ::_thesis: verum end; begin theorem :: JORDAN1I:4 for f being non constant standard special_circular_sequence for p being Point of (TOP-REAL 2) st p in rng f holds left_cell (f,(p .. f)) = left_cell ((Rotate (f,p)),1) proof set n = 1; let f be non constant standard special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f holds left_cell (f,(p .. f)) = left_cell ((Rotate (f,p)),1) let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f implies left_cell (f,(p .. f)) = left_cell ((Rotate (f,p)),1) ) assume A1: p in rng f ; ::_thesis: left_cell (f,(p .. f)) = left_cell ((Rotate (f,p)),1) set k = p .. f; len f > 1 by GOBOARD7:34, XXREAL_0:2; then p .. f < len f by A1, SPRECT_5:7; then A2: (p .. f) + 1 <= len f by NAT_1:13; A3: 1 <= p .. f by A1, FINSEQ_4:21; A4: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) & (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j2) ) proof (Rotate (f,p)) /. (((1 + 1) + (p .. f)) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1) by NAT_D:34; then A5: (Rotate (f,p)) /. ((((p .. f) + 1) + 1) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1) ; A6: left_cell (f,(p .. f)) = left_cell (f,(p .. f)) ; let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) & (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) ) implies ( i1 = i2 & j1 = j2 + 1 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j2) ) ) assume that A7: ( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) ) and A8: (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) and A9: (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) ; ::_thesis: ( ( i1 = i2 & j1 + 1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) ) or ( i1 + 1 = i2 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) or ( i1 = i2 + 1 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j2) ) ) A10: GoB (Rotate (f,p)) = GoB f by REVROT_1:28; len (Rotate (f,p)) = len f by REVROT_1:14; then (Rotate (f,p)) /. (len f) = (Rotate (f,p)) /. 1 by FINSEQ_6:def_1; then (Rotate (f,p)) /. (((p .. f) + (len f)) -' (p .. f)) = (Rotate (f,p)) /. 1 by NAT_D:34; then A11: f /. (p .. f) = (GoB f) * (i1,j1) by A1, A3, A8, A10, REVROT_1:18; p .. f < (p .. f) + 1 by NAT_1:13; then A12: f /. ((p .. f) + 1) = (GoB f) * (i2,j2) by A1, A2, A9, A10, A5, REVROT_1:10; then A13: ( ( i1 = i2 & j1 + 1 = j2 & left_cell (f,(p .. f)) = cell ((GoB f),(i1 -' 1),j1) ) or ( i1 + 1 = i2 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB f),i1,j1) ) or ( i1 = i2 + 1 & j1 = j2 & left_cell (f,(p .. f)) = cell ((GoB f),i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell (f,(p .. f)) = cell ((GoB f),i1,j2) ) ) by A3, A2, A7, A10, A11, A6, GOBOARD5:def_7; 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 A3, A2, A7, A10, A11, A12, A6, GOBOARD5:def_7; case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) hence left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j1) by A13, REVROT_1:28; ::_thesis: verum end; case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) hence left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) by A13, REVROT_1:28; ::_thesis: verum end; case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) hence left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,(j2 -' 1)) by A13, REVROT_1:28; ::_thesis: verum end; case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j2) hence left_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j2) by A13, REVROT_1:28; ::_thesis: verum end; end; end; 1 + 1 <= len (Rotate (f,p)) by GOBOARD7:34, XXREAL_0:2; hence left_cell (f,(p .. f)) = left_cell ((Rotate (f,p)),1) by A4, GOBOARD5:def_7; ::_thesis: verum end; theorem Th5: :: JORDAN1I:5 for f being non constant standard special_circular_sequence for p being Point of (TOP-REAL 2) st p in rng f holds right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1) proof set n = 1; let f be non constant standard special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f holds right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1) let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f implies right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1) ) assume A1: p in rng f ; ::_thesis: right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1) set k = p .. f; len f > 1 by GOBOARD7:34, XXREAL_0:2; then p .. f < len f by A1, SPRECT_5:7; then A2: (p .. f) + 1 <= len f by NAT_1:13; A3: 1 <= p .. f by A1, FINSEQ_4:21; A4: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) & (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2) ) proof (Rotate (f,p)) /. (((1 + 1) + (p .. f)) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1) by NAT_D:34; then A5: (Rotate (f,p)) /. ((((p .. f) + 1) + 1) -' (p .. f)) = (Rotate (f,p)) /. (1 + 1) ; A6: right_cell (f,(p .. f)) = right_cell (f,(p .. f)) ; let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) & (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) & (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2) ) implies ( i1 = i2 & j1 = j2 + 1 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2) ) ) assume that A7: ( [i1,j1] in Indices (GoB (Rotate (f,p))) & [i2,j2] in Indices (GoB (Rotate (f,p))) ) and A8: (Rotate (f,p)) /. 1 = (GoB (Rotate (f,p))) * (i1,j1) and A9: (Rotate (f,p)) /. (1 + 1) = (GoB (Rotate (f,p))) * (i2,j2) ; ::_thesis: ( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2) ) ) A10: GoB (Rotate (f,p)) = GoB f by REVROT_1:28; len (Rotate (f,p)) = len f by REVROT_1:14; then (Rotate (f,p)) /. (len f) = (Rotate (f,p)) /. 1 by FINSEQ_6:def_1; then (Rotate (f,p)) /. (((p .. f) + (len f)) -' (p .. f)) = (Rotate (f,p)) /. 1 by NAT_D:34; then A11: f /. (p .. f) = (GoB f) * (i1,j1) by A1, A3, A8, A10, REVROT_1:18; p .. f < (p .. f) + 1 by NAT_1:13; then A12: f /. ((p .. f) + 1) = (GoB f) * (i2,j2) by A1, A2, A9, A10, A5, REVROT_1:10; then A13: ( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,(p .. f)) = cell ((GoB f),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB f),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,(p .. f)) = cell ((GoB f),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,(p .. f)) = cell ((GoB f),(i1 -' 1),j2) ) ) by A3, A2, A7, A10, A11, A6, GOBOARD5:def_6; 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 A3, A2, A7, A10, A11, A12, A6, GOBOARD5:def_6; case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) hence right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,j1) by A13, REVROT_1:28; ::_thesis: verum end; case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1)) hence right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i1,(j1 -' 1)) by A13, REVROT_1:28; ::_thesis: verum end; case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2) hence right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),i2,j2) by A13, REVROT_1:28; ::_thesis: verum end; case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2) hence right_cell (f,(p .. f)) = cell ((GoB (Rotate (f,p))),(i1 -' 1),j2) by A13, REVROT_1:28; ::_thesis: verum end; end; end; 1 + 1 <= len (Rotate (f,p)) by GOBOARD7:34, XXREAL_0:2; hence right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1) by A4, GOBOARD5:def_6; ::_thesis: verum end; theorem :: JORDAN1I:6 for n being Element of NAT for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1) proof let n be Element of NAT ; ::_thesis: for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1) let C be non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1) set f = Cage (C,n); set G = Gauge (C,n); consider j being Element of NAT such that A1: 1 <= j and A2: j <= width (Gauge (C,n)) and A3: W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) by JORDAN1D:30; A4: len (Gauge (C,n)) >= 4 by JORDAN8:10; then A5: 1 <= len (Gauge (C,n)) by XXREAL_0:2; set k = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)); A6: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43; then A7: ( (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) & (Cage (C,n)) . ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = W-min (L~ (Cage (C,n))) ) by FINSEQ_4:19, FINSEQ_4:20; then A8: (Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = W-min (L~ (Cage (C,n))) by PARTFUN1:def_6; A9: now__::_thesis:_not_(W-min_(L~_(Cage_(C,n))))_.._(Cage_(C,n))_=_len_(Cage_(C,n)) A10: 1 < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th1; A11: 1 in dom (Cage (C,n)) by A6, FINSEQ_3:31; assume (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n)) ; ::_thesis: contradiction then (Cage (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by A8, FINSEQ_6:def_1; then (Cage (C,n)) . 1 = W-min (L~ (Cage (C,n))) by A11, PARTFUN1:def_6; hence contradiction by A11, A10, FINSEQ_4:24; ::_thesis: verum end; 1 <= len (Gauge (C,n)) by A4, XXREAL_0:2; then A12: [1,j] in Indices (Gauge (C,n)) by A1, A2, MATRIX_1:36; then A13: [1,j] in Indices (GoB (Cage (C,n))) by JORDAN1H:44; (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= len (Cage (C,n)) by A6, FINSEQ_4:21; then (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A9, XXREAL_0:1; then A14: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13; (Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (1,j) by A3, A7, PARTFUN1:def_6; then A15: (Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * (1,j) by JORDAN1H:44; set p = W-min C; A16: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; A17: 1 <= ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:11; then A18: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A14, FINSEQ_3:25; A19: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A14, A17, FINSEQ_3:25; then consider ki, kj being Element of NAT such that A20: [ki,kj] in Indices (Gauge (C,n)) and A21: (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (ki,kj) by A16, GOBOARD1:def_9; A22: ( 1 <= kj & ki <= len (Gauge (C,n)) ) by A20, MATRIX_1:38; A23: 1 <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th1; then A24: ((Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = W-bound (L~ (Cage (C,n))) by A8, A14, JORDAN1E:22; then ((Gauge (C,n)) * (1,j)) `1 = ((Gauge (C,n)) * (ki,kj)) `1 by A3, A21, EUCLID:52; then A25: ki = 1 by A20, A12, JORDAN1G:7; 2 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2; then (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in W-most (L~ (Cage (C,n))) by A24, A19, GOBOARD1:1, SPRECT_2:12; then ((Gauge (C,n)) * (1,j)) `2 <= ((Gauge (C,n)) * (ki,kj)) `2 by A3, A21, PSCOMP_1:31; then A26: j <= kj by A2, A25, A22, GOBOARD5:4; ( [ki,kj] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (GoB (Cage (C,n))) * (ki,kj) ) by A20, A21, JORDAN1H:44; then (abs (1 - ki)) + (abs (j - kj)) = 1 by A6, A18, A13, A15, FINSEQ_4:20, GOBOARD5:12; then A27: 0 + (abs (j - kj)) = 1 by A25, ABSVALUE:2; then A28: (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (1,(j + 1)) by A21, A25, A26, SEQM_3:41; A29: kj = j + 1 by A26, A27, SEQM_3:41; then ( 1 <= j + 1 & j + 1 <= width (Gauge (C,n)) ) by A20, MATRIX_1:38; then [1,(j + 1)] in Indices (Gauge (C,n)) by A5, MATRIX_1:36; then A30: right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),1,j) by A3, A16, A23, A8, A14, A12, A28, GOBRD13:22; A31: now__::_thesis:_W-min_C_in_right_cell_((Cage_(C,n)),((W-min_(L~_(Cage_(C,n))))_.._(Cage_(C,n))),(Gauge_(C,n))) len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; then A32: j + 1 <= len (Gauge (C,n)) by A20, A29, MATRIX_1:38; 1 <= j + 1 by A20, A29, MATRIX_1:38; then A33: ((Gauge (C,n)) * (2,(j + 1))) `1 = W-bound C by A32, JORDAN8:11; assume A34: not W-min C in right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) ; ::_thesis: contradiction j + 1 <= width (Gauge (C,n)) by A20, A29, MATRIX_1:38; then A35: j < width (Gauge (C,n)) by NAT_1:13; A36: 2 <= len (Gauge (C,n)) by A4, XXREAL_0:2; 1 < len (Gauge (C,n)) by A4, XXREAL_0:2; then LSeg (((Gauge (C,n)) * ((1 + 1),j)),((Gauge (C,n)) * ((1 + 1),(j + 1)))) c= cell ((Gauge (C,n)),1,j) by A1, A35, GOBOARD5:18; then A37: not W-min C in LSeg (((Gauge (C,n)) * (2,j)),((Gauge (C,n)) * (2,(j + 1)))) by A30, A34; A38: ( 1 <= j + 1 & j + 1 <= width (Gauge (C,n)) ) by A20, A29, MATRIX_1:38; j <= len (Gauge (C,n)) by A2, JORDAN8:def_1; then A39: ((Gauge (C,n)) * (2,j)) `1 = W-bound C by A1, JORDAN8:11; (W-min C) `1 = W-bound C by EUCLID:52; then A40: ( (W-min C) `2 > ((Gauge (C,n)) * (2,(j + 1))) `2 or (W-min C) `2 < ((Gauge (C,n)) * (2,j)) `2 ) by A37, A39, A33, GOBOARD7:7; percases ( (W-min C) `2 > ((Gauge (C,n)) * (1,(j + 1))) `2 or (W-min C) `2 < ((Gauge (C,n)) * (1,j)) `2 ) by A1, A2, A40, A38, A36, GOBOARD5:1; supposeA41: (W-min C) `2 > ((Gauge (C,n)) * (1,(j + 1))) `2 ; ::_thesis: contradiction cell ((Gauge (C,n)),1,j) meets C by A23, A14, A30, JORDAN9:31; then (cell ((Gauge (C,n)),1,j)) /\ C <> {} by XBOOLE_0:def_7; then consider c being set such that A42: c in (cell ((Gauge (C,n)),1,j)) /\ C by XBOOLE_0:def_1; reconsider c = c as Element of (TOP-REAL 2) by A42; A43: c in cell ((Gauge (C,n)),1,j) by A42, XBOOLE_0:def_4; A44: c in C by A42, XBOOLE_0:def_4; then A45: c `1 >= W-bound C by PSCOMP_1:24; A46: ( 1 + 1 <= len (Gauge (C,n)) & j + 1 <= width (Gauge (C,n)) ) by A4, A20, A29, MATRIX_1:38, XXREAL_0:2; then c `1 <= ((Gauge (C,n)) * ((1 + 1),j)) `1 by A1, A43, JORDAN9:17; then c in W-most C by A39, A44, A45, SPRECT_2:12, XXREAL_0:1; then A47: c `2 >= (W-min C) `2 by PSCOMP_1:31; c `2 <= ((Gauge (C,n)) * (1,(j + 1))) `2 by A1, A43, A46, JORDAN9:17; hence contradiction by A41, A47, XXREAL_0:2; ::_thesis: verum end; supposeA48: (W-min C) `2 < ((Gauge (C,n)) * (1,j)) `2 ; ::_thesis: contradiction west_halfline (W-min C) meets L~ (Cage (C,n)) by JORDAN1A:54, SPRECT_1:13; then consider r being set such that A49: r in west_halfline (W-min C) and A50: r in L~ (Cage (C,n)) by XBOOLE_0:3; reconsider r = r as Element of (TOP-REAL 2) by A49; r in (west_halfline (W-min C)) /\ (L~ (Cage (C,n))) by A49, A50, XBOOLE_0:def_4; then r `1 = W-bound (L~ (Cage (C,n))) by JORDAN1A:85, PSCOMP_1:34; then r in W-most (L~ (Cage (C,n))) by A50, SPRECT_2:12; then (W-min (L~ (Cage (C,n)))) `2 <= r `2 by PSCOMP_1:31; hence contradiction by A3, A48, A49, TOPREAL1:def_13; ::_thesis: verum end; end; end; GoB (Cage (C,n)) = Gauge (C,n) by JORDAN1H:44; then W-min C in right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A23, A14, A31, JORDAN1H:23; hence W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1) by A6, Th5; ::_thesis: verum end; theorem :: JORDAN1I:7 for n being Element of NAT for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) proof let n be Element of NAT ; ::_thesis: for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) let C be non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) set f = Cage (C,n); set G = Gauge (C,n); consider j being Element of NAT such that A1: 1 <= j and A2: j <= width (Gauge (C,n)) and A3: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by JORDAN1D:25; A4: len (Gauge (C,n)) >= 4 by JORDAN8:10; then A5: 1 <= len (Gauge (C,n)) by XXREAL_0:2; set k = (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)); A6: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46; then A7: ( (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) & (Cage (C,n)) . ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = E-max (L~ (Cage (C,n))) ) by FINSEQ_4:19, FINSEQ_4:20; then A8: (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = E-max (L~ (Cage (C,n))) by PARTFUN1:def_6; A9: now__::_thesis:_not_(E-max_(L~_(Cage_(C,n))))_.._(Cage_(C,n))_=_len_(Cage_(C,n)) A10: 1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th2; A11: 1 in dom (Cage (C,n)) by A6, FINSEQ_3:31; assume (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n)) ; ::_thesis: contradiction then (Cage (C,n)) /. 1 = E-max (L~ (Cage (C,n))) by A8, FINSEQ_6:def_1; then (Cage (C,n)) . 1 = E-max (L~ (Cage (C,n))) by A11, PARTFUN1:def_6; hence contradiction by A11, A10, FINSEQ_4:24; ::_thesis: verum end; (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by A3, A7, PARTFUN1:def_6; then A12: (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * ((len (Gauge (C,n))),j) by JORDAN1H:44; (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= len (Cage (C,n)) by A6, FINSEQ_4:21; then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A9, XXREAL_0:1; then A13: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13; A14: 1 <= len (Gauge (C,n)) by A4, XXREAL_0:2; then A15: [(len (Gauge (C,n))),j] in Indices (Gauge (C,n)) by A1, A2, MATRIX_1:36; ( 1 <= (j -' 1) + 1 & (j -' 1) + 1 <= width (Gauge (C,n)) ) by A1, A2, XREAL_1:235; then A16: [(len (Gauge (C,n))),((j -' 1) + 1)] in Indices (Gauge (C,n)) by A14, MATRIX_1:36; set p = E-max C; A17: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; A18: 1 <= ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:11; then A19: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A13, FINSEQ_3:25; A20: ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A13, A18, FINSEQ_3:25; then consider ki, kj being Element of NAT such that A21: [ki,kj] in Indices (Gauge (C,n)) and A22: (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (ki,kj) by A17, GOBOARD1:def_9; A23: ( [ki,kj] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (GoB (Cage (C,n))) * (ki,kj) ) by A21, A22, JORDAN1H:44; A24: 1 <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th2; then A25: ((Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = E-bound (L~ (Cage (C,n))) by A8, A13, JORDAN1E:20; then ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 = ((Gauge (C,n)) * (ki,kj)) `1 by A3, A22, EUCLID:52; then A26: ki = len (Gauge (C,n)) by A21, A15, JORDAN1G:7; A27: ( kj <= width (Gauge (C,n)) & 1 <= ki ) by A21, MATRIX_1:38; [(len (Gauge (C,n))),j] in Indices (GoB (Cage (C,n))) by A15, JORDAN1H:44; then (abs ((len (Gauge (C,n))) - ki)) + (abs (j - kj)) = 1 by A6, A19, A12, A23, FINSEQ_4:20, GOBOARD5:12; then A28: 0 + (abs (j - kj)) = 1 by A26, ABSVALUE:2; 2 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2; then (Cage (C,n)) /. (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in E-most (L~ (Cage (C,n))) by A25, A20, GOBOARD1:1, SPRECT_2:13; then ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 >= ((Gauge (C,n)) * (ki,kj)) `2 by A3, A22, PSCOMP_1:47; then j >= kj by A1, A26, A27, GOBOARD5:4; then j = kj + 1 by A28, SEQM_3:41; then kj = j - 1 ; then A29: kj = j -' 1 by A1, XREAL_1:233; then A30: 1 <= j -' 1 by A21, MATRIX_1:38; A31: j -' 1 <= width (Gauge (C,n)) by A21, A29, MATRIX_1:38; (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),((j -' 1) + 1)) by A1, A3, A8, XREAL_1:235; then A32: right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by A17, A24, A13, A21, A22, A26, A29, A16, GOBRD13:28; A33: now__::_thesis:_E-max_C_in_right_cell_((Cage_(C,n)),((E-max_(L~_(Cage_(C,n))))_.._(Cage_(C,n))),(Gauge_(C,n))) j -' 1 <= len (Gauge (C,n)) by A31, JORDAN8:def_1; then A34: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `1 = E-bound C by A30, JORDAN8:12; j <= len (Gauge (C,n)) by A2, JORDAN8:def_1; then A35: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `1 = E-bound C by A1, JORDAN8:12; assume A36: not E-max C in right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) ; ::_thesis: contradiction A37: 1 < len (Gauge (C,n)) by A4, XXREAL_0:2; then A38: 1 <= (len (Gauge (C,n))) -' 1 by NAT_D:49; A39: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:50; then A40: ( ((Gauge (C,n)) * (1,j)) `2 = ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `2 & ((Gauge (C,n)) * (1,(j -' 1))) `2 = ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 ) by A1, A2, A30, A31, A38, GOBOARD5:1; j -' 1 < j by A30, NAT_D:51; then j -' 1 < width (Gauge (C,n)) by A2, XXREAL_0:2; then LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),((j -' 1) + 1)))) c= cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by A30, A38, A39, GOBOARD5:19; then not E-max C in LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),((j -' 1) + 1)))) by A32, A36; then A41: not E-max C in LSeg (((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))),((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j))) by A1, XREAL_1:235; (E-max C) `1 = E-bound C by EUCLID:52; then A42: ( (E-max C) `2 > ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),j)) `2 or (E-max C) `2 < ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 ) by A41, A34, A35, GOBOARD7:7; percases ( (E-max C) `2 < ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 or (E-max C) `2 > ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 ) by A1, A2, A5, A30, A31, A42, A40, GOBOARD5:1; supposeA43: (E-max C) `2 < ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 ; ::_thesis: contradiction A44: ( 1 <= j -' 1 & (j -' 1) + 1 <= width (Gauge (C,n)) ) by A1, A2, A21, A29, MATRIX_1:38, XREAL_1:235; cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) meets C by A24, A13, A32, JORDAN9:31; then (cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1))) /\ C <> {} by XBOOLE_0:def_7; then consider c being set such that A45: c in (cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1))) /\ C by XBOOLE_0:def_1; reconsider c = c as Element of (TOP-REAL 2) by A45; A46: ( 1 <= (len (Gauge (C,n))) -' 1 & ((len (Gauge (C,n))) -' 1) + 1 <= len (Gauge (C,n)) ) by A37, NAT_D:49, XREAL_1:235; A47: c in cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),(j -' 1)) by A45, XBOOLE_0:def_4; then A48: ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `1 <= c `1 by A46, A44, JORDAN9:17; A49: c in C by A45, XBOOLE_0:def_4; then c `1 <= E-bound C by PSCOMP_1:24; then c in E-most C by A34, A49, A48, SPRECT_2:13, XXREAL_0:1; then A50: c `2 <= (E-max C) `2 by PSCOMP_1:47; ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),(j -' 1))) `2 <= c `2 by A47, A46, A44, JORDAN9:17; then ((Gauge (C,n)) * (1,(j -' 1))) `2 <= c `2 by A30, A31, A38, A39, GOBOARD5:1; then ((Gauge (C,n)) * ((len (Gauge (C,n))),(j -' 1))) `2 <= c `2 by A5, A30, A31, GOBOARD5:1; hence contradiction by A43, A50, XXREAL_0:2; ::_thesis: verum end; supposeA51: (E-max C) `2 > ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `2 ; ::_thesis: contradiction east_halfline (E-max C) meets L~ (Cage (C,n)) by JORDAN1A:52, SPRECT_1:14; then consider r being set such that A52: r in east_halfline (E-max C) and A53: r in L~ (Cage (C,n)) by XBOOLE_0:3; reconsider r = r as Element of (TOP-REAL 2) by A52; r in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A52, A53, XBOOLE_0:def_4; then r `1 = E-bound (L~ (Cage (C,n))) by JORDAN1A:83, PSCOMP_1:50; then r in E-most (L~ (Cage (C,n))) by A53, SPRECT_2:13; then (E-max (L~ (Cage (C,n)))) `2 >= r `2 by PSCOMP_1:47; hence contradiction by A3, A51, A52, TOPREAL1:def_11; ::_thesis: verum end; end; end; GoB (Cage (C,n)) = Gauge (C,n) by JORDAN1H:44; then E-max C in right_cell ((Cage (C,n)),((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A24, A13, A33, JORDAN1H:23; hence E-max C in right_cell ((Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))),1) by A6, Th5; ::_thesis: verum end; theorem :: JORDAN1I:8 for n being Element of NAT for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (L~ (Cage (C,n)))))),1) proof let n be Element of NAT ; ::_thesis: for C being non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (L~ (Cage (C,n)))))),1) let C be non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (L~ (Cage (C,n)))))),1) set f = Cage (C,n); set G = Gauge (C,n); consider j being Element of NAT such that A1: 1 <= j and A2: j <= len (Gauge (C,n)) and A3: S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (j,1) by JORDAN1D:28; A4: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; set k = (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)); A5: S-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:42; then A6: ( (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) & (Cage (C,n)) . ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = S-max (L~ (Cage (C,n))) ) by FINSEQ_4:19, FINSEQ_4:20; then A7: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = S-max (L~ (Cage (C,n))) by PARTFUN1:def_6; A8: now__::_thesis:_not_(S-max_(L~_(Cage_(C,n))))_.._(Cage_(C,n))_=_len_(Cage_(C,n)) A9: 1 < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th3; A10: 1 in dom (Cage (C,n)) by A5, FINSEQ_3:31; assume (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n)) ; ::_thesis: contradiction then (Cage (C,n)) /. 1 = S-max (L~ (Cage (C,n))) by A7, FINSEQ_6:def_1; then (Cage (C,n)) . 1 = S-max (L~ (Cage (C,n))) by A10, PARTFUN1:def_6; hence contradiction by A10, A9, FINSEQ_4:24; ::_thesis: verum end; (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= len (Cage (C,n)) by A5, FINSEQ_4:21; then (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A8, XXREAL_0:1; then A11: ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13; A12: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (((j -' 1) + 1),1) by A1, A3, A7, XREAL_1:235; (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (j,1) by A3, A6, PARTFUN1:def_6; then A13: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * (j,1) by JORDAN1H:44; set p = S-max C; A14: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A15: len (Gauge (C,n)) >= 4 by JORDAN8:10; then A16: 1 <= len (Gauge (C,n)) by XXREAL_0:2; A17: 1 <= ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:11; then A18: ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A11, FINSEQ_3:25; A19: ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A11, A17, FINSEQ_3:25; then consider kj, ki being Element of NAT such that A20: [kj,ki] in Indices (Gauge (C,n)) and A21: (Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (kj,ki) by A4, GOBOARD1:def_9; A22: ( [kj,ki] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (GoB (Cage (C,n))) * (kj,ki) ) by A20, A21, JORDAN1H:44; A23: ki <= width (Gauge (C,n)) by A20, MATRIX_1:38; A24: 1 <= kj by A20, MATRIX_1:38; len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; then A25: [j,1] in Indices (Gauge (C,n)) by A1, A2, A16, MATRIX_1:36; then A26: [((j -' 1) + 1),1] in Indices (Gauge (C,n)) by A1, XREAL_1:235; A27: 1 <= (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th3; then A28: ((Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `2 = S-bound (L~ (Cage (C,n))) by A7, A11, JORDAN1E:21; then ((Gauge (C,n)) * (j,1)) `2 = ((Gauge (C,n)) * (kj,ki)) `2 by A3, A21, EUCLID:52; then A29: ki = 1 by A20, A25, JORDAN1G:6; [j,1] in Indices (GoB (Cage (C,n))) by A25, JORDAN1H:44; then (abs (1 - ki)) + (abs (j - kj)) = 1 by A5, A18, A13, A22, FINSEQ_4:20, GOBOARD5:12; then A30: 0 + (abs (j - kj)) = 1 by A29, ABSVALUE:2; A31: kj <= len (Gauge (C,n)) by A20, MATRIX_1:38; 2 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2; then (Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in S-most (L~ (Cage (C,n))) by A28, A19, GOBOARD1:1, SPRECT_2:11; then ((Gauge (C,n)) * (j,1)) `1 >= ((Gauge (C,n)) * (kj,ki)) `1 by A3, A21, PSCOMP_1:55; then kj <= j by A1, A29, A23, A31, GOBOARD5:3; then kj + 1 = j by A30, SEQM_3:41; then A32: kj = j - 1 ; then kj = j -' 1 by A24, NAT_D:39; then A33: [(j -' 1),1] in Indices (Gauge (C,n)) by A16, A24, A31, A14, MATRIX_1:36; (Cage (C,n)) /. (((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * ((j -' 1),1) by A21, A29, A24, A32, NAT_D:39; then A34: right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),(j -' 1),1) by A4, A27, A11, A33, A26, A12, GOBRD13:26; A35: now__::_thesis:_S-max_C_in_right_cell_((Cage_(C,n)),((S-max_(L~_(Cage_(C,n))))_.._(Cage_(C,n))),(Gauge_(C,n))) 1 < len (Gauge (C,n)) by A15, XXREAL_0:2; then A36: 1 < width (Gauge (C,n)) by JORDAN8:def_1; assume A37: not S-max C in right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) ; ::_thesis: contradiction A38: 1 <= j -' 1 by A24, A32, NAT_D:39; then j -' 1 < j by NAT_D:51; then j -' 1 < len (Gauge (C,n)) by A2, XXREAL_0:2; then LSeg (((Gauge (C,n)) * ((j -' 1),(1 + 1))),((Gauge (C,n)) * (((j -' 1) + 1),(1 + 1)))) c= cell ((Gauge (C,n)),(j -' 1),1) by A36, A38, GOBOARD5:21; then LSeg (((Gauge (C,n)) * ((j -' 1),2)),((Gauge (C,n)) * (j,2))) c= cell ((Gauge (C,n)),(j -' 1),1) by A1, XREAL_1:235; then A39: not S-max C in LSeg (((Gauge (C,n)) * ((j -' 1),2)),((Gauge (C,n)) * (j,2))) by A34, A37; len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; then A40: 2 <= width (Gauge (C,n)) by A15, XXREAL_0:2; A41: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A42: j -' 1 <= len (Gauge (C,n)) by A24, A31, A32, NAT_D:39; then A43: ((Gauge (C,n)) * ((j -' 1),2)) `2 = S-bound C by A38, JORDAN8:13; ( ((Gauge (C,n)) * (j,2)) `2 = S-bound C & (S-max C) `2 = S-bound C ) by A1, A2, EUCLID:52, JORDAN8:13; then A44: ( (S-max C) `1 > ((Gauge (C,n)) * (j,2)) `1 or (S-max C) `1 < ((Gauge (C,n)) * ((j -' 1),2)) `1 ) by A39, A43, GOBOARD7:8; percases ( (S-max C) `1 < ((Gauge (C,n)) * ((j -' 1),1)) `1 or (S-max C) `1 > ((Gauge (C,n)) * (j,1)) `1 ) by A1, A2, A38, A42, A44, A40, GOBOARD5:2; supposeA45: (S-max C) `1 < ((Gauge (C,n)) * ((j -' 1),1)) `1 ; ::_thesis: contradiction cell ((Gauge (C,n)),(j -' 1),1) meets C by A27, A11, A34, JORDAN9:31; then (cell ((Gauge (C,n)),(j -' 1),1)) /\ C <> {} by XBOOLE_0:def_7; then consider c being set such that A46: c in (cell ((Gauge (C,n)),(j -' 1),1)) /\ C by XBOOLE_0:def_1; reconsider c = c as Element of (TOP-REAL 2) by A46; A47: c in cell ((Gauge (C,n)),(j -' 1),1) by A46, XBOOLE_0:def_4; A48: c in C by A46, XBOOLE_0:def_4; then A49: c `2 >= S-bound C by PSCOMP_1:24; A50: ( (j -' 1) + 1 <= len (Gauge (C,n)) & 1 + 1 <= width (Gauge (C,n)) ) by A1, A2, A15, A41, XREAL_1:235, XXREAL_0:2; then c `2 <= ((Gauge (C,n)) * ((j -' 1),(1 + 1))) `2 by A38, A47, JORDAN9:17; then c in S-most C by A43, A48, A49, SPRECT_2:11, XXREAL_0:1; then A51: c `1 <= (S-max C) `1 by PSCOMP_1:55; ((Gauge (C,n)) * ((j -' 1),1)) `1 <= c `1 by A38, A47, A50, JORDAN9:17; hence contradiction by A45, A51, XXREAL_0:2; ::_thesis: verum end; supposeA52: (S-max C) `1 > ((Gauge (C,n)) * (j,1)) `1 ; ::_thesis: contradiction south_halfline (S-max C) meets L~ (Cage (C,n)) by JORDAN1A:53, SPRECT_1:12; then consider r being set such that A53: r in south_halfline (S-max C) and A54: r in L~ (Cage (C,n)) by XBOOLE_0:3; reconsider r = r as Element of (TOP-REAL 2) by A53; r in (south_halfline (S-max C)) /\ (L~ (Cage (C,n))) by A53, A54, XBOOLE_0:def_4; then r `2 = S-bound (L~ (Cage (C,n))) by JORDAN1A:84, PSCOMP_1:58; then r in S-most (L~ (Cage (C,n))) by A54, SPRECT_2:11; then (S-max (L~ (Cage (C,n)))) `1 >= r `1 by PSCOMP_1:55; hence contradiction by A3, A52, A53, TOPREAL1:def_12; ::_thesis: verum end; end; end; GoB (Cage (C,n)) = Gauge (C,n) by JORDAN1H:44; then S-max C in right_cell ((Cage (C,n)),((S-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A27, A11, A35, JORDAN1H:23; hence S-max C in right_cell ((Rotate ((Cage (C,n)),(S-max (L~ (Cage (C,n)))))),1) by A5, Th5; ::_thesis: verum end; begin theorem Th9: :: JORDAN1I:9 for f being non constant standard clockwise_oriented special_circular_sequence for p being Point of (TOP-REAL 2) st p `1 < W-bound (L~ f) holds p in LeftComp f proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st p `1 < W-bound (L~ f) holds p in LeftComp f let p be Point of (TOP-REAL 2); ::_thesis: ( p `1 < W-bound (L~ f) implies p in LeftComp f ) set g = Rotate (f,(N-min (L~ f))); A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33; assume A2: p `1 < W-bound (L~ f) ; ::_thesis: p in LeftComp f N-min (L~ f) in rng f by SPRECT_2:39; then (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92; then p in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:110; hence p in LeftComp f by REVROT_1:36; ::_thesis: verum end; theorem Th10: :: JORDAN1I:10 for f being non constant standard clockwise_oriented special_circular_sequence for p being Point of (TOP-REAL 2) st p `1 > E-bound (L~ f) holds p in LeftComp f proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st p `1 > E-bound (L~ f) holds p in LeftComp f let p be Point of (TOP-REAL 2); ::_thesis: ( p `1 > E-bound (L~ f) implies p in LeftComp f ) set g = Rotate (f,(N-min (L~ f))); A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33; assume A2: p `1 > E-bound (L~ f) ; ::_thesis: p in LeftComp f N-min (L~ f) in rng f by SPRECT_2:39; then (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92; then p in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:111; hence p in LeftComp f by REVROT_1:36; ::_thesis: verum end; theorem Th11: :: JORDAN1I:11 for f being non constant standard clockwise_oriented special_circular_sequence for p being Point of (TOP-REAL 2) st p `2 < S-bound (L~ f) holds p in LeftComp f proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st p `2 < S-bound (L~ f) holds p in LeftComp f let p be Point of (TOP-REAL 2); ::_thesis: ( p `2 < S-bound (L~ f) implies p in LeftComp f ) set g = Rotate (f,(N-min (L~ f))); A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33; assume A2: p `2 < S-bound (L~ f) ; ::_thesis: p in LeftComp f N-min (L~ f) in rng f by SPRECT_2:39; then (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92; then p in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:112; hence p in LeftComp f by REVROT_1:36; ::_thesis: verum end; theorem Th12: :: JORDAN1I:12 for f being non constant standard clockwise_oriented special_circular_sequence for p being Point of (TOP-REAL 2) st p `2 > N-bound (L~ f) holds p in LeftComp f proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for p being Point of (TOP-REAL 2) st p `2 > N-bound (L~ f) holds p in LeftComp f let p be Point of (TOP-REAL 2); ::_thesis: ( p `2 > N-bound (L~ f) implies p in LeftComp f ) set g = Rotate (f,(N-min (L~ f))); A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33; assume A2: p `2 > N-bound (L~ f) ; ::_thesis: p in LeftComp f N-min (L~ f) in rng f by SPRECT_2:39; then (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92; then p in LeftComp (Rotate (f,(N-min (L~ f)))) by A1, A2, JORDAN2C:113; hence p in LeftComp f by REVROT_1:36; ::_thesis: verum end; theorem Th13: :: JORDAN1I:13 for f being non constant standard clockwise_oriented special_circular_sequence for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds j < width G proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds j < width G let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds j < width G ) assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds j < width G let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) implies j < width G ) assume that A2: ( 1 <= k & k + 1 <= len f ) and A3: [i,j] in Indices G and A4: ( [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) ) ; ::_thesis: j < width G assume A5: j >= width G ; ::_thesis: contradiction j <= width G by A3, MATRIX_1:38; then A6: j = width G by A5, XXREAL_0:1; A7: i <= len G by A3, MATRIX_1:38; right_cell (f,k,G) = cell (G,i,j) by A1, A2, A3, A4, GOBRD13:26; then not (right_cell (f,k,G)) \ (L~ f) is bounded by A7, A6, JORDAN1A:27, TOPREAL6:90; then not RightComp f is bounded by A1, A2, JORDAN9:27, RLTOPSP1:42; then not BDD (L~ f) is bounded by GOBRD14:37; hence contradiction by JORDAN2C:106; ::_thesis: verum end; theorem Th14: :: JORDAN1I:14 for f being non constant standard clockwise_oriented special_circular_sequence for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds i < len G proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds i < len G let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds i < len G ) assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds i < len G let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) implies i < len G ) assume that A2: ( 1 <= k & k + 1 <= len f ) and A3: [i,j] in Indices G and A4: ( [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) ) ; ::_thesis: i < len G assume A5: i >= len G ; ::_thesis: contradiction i <= len G by A3, MATRIX_1:38; then A6: i = len G by A5, XXREAL_0:1; A7: j <= width G by A3, MATRIX_1:38; right_cell (f,k,G) = cell (G,i,j) by A1, A2, A3, A4, GOBRD13:22; then not (right_cell (f,k,G)) \ (L~ f) is bounded by A7, A6, JORDAN1B:34, TOPREAL6:90; then not RightComp f is bounded by A1, A2, JORDAN9:27, RLTOPSP1:42; then not BDD (L~ f) is bounded by GOBRD14:37; hence contradiction by JORDAN2C:106; ::_thesis: verum end; theorem Th15: :: JORDAN1I:15 for f being non constant standard clockwise_oriented special_circular_sequence for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds j > 1 proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds j > 1 let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds j > 1 ) assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds j > 1 let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) implies j > 1 ) assume that A2: ( 1 <= k & k + 1 <= len f ) and A3: [i,j] in Indices G and A4: ( [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) ) ; ::_thesis: j > 1 assume A5: j <= 1 ; ::_thesis: contradiction 1 <= j by A3, MATRIX_1:38; then j = 1 by A5, XXREAL_0:1; then A6: j -' 1 = 0 by XREAL_1:232; A7: i <= len G by A3, MATRIX_1:38; right_cell (f,k,G) = cell (G,i,(j -' 1)) by A1, A2, A3, A4, GOBRD13:24; then not (right_cell (f,k,G)) \ (L~ f) is bounded by A7, A6, JORDAN1A:26, TOPREAL6:90; then not RightComp f is bounded by A1, A2, JORDAN9:27, RLTOPSP1:42; then not BDD (L~ f) is bounded by GOBRD14:37; hence contradiction by JORDAN2C:106; ::_thesis: verum end; theorem Th16: :: JORDAN1I:16 for f being non constant standard clockwise_oriented special_circular_sequence for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds i > 1 proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds i > 1 let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds i > 1 ) assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds i > 1 let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) implies i > 1 ) assume that A2: ( 1 <= k & k + 1 <= len f ) and A3: [i,j] in Indices G and A4: ( [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) ) ; ::_thesis: i > 1 assume A5: i <= 1 ; ::_thesis: contradiction 1 <= i by A3, MATRIX_1:38; then i = 1 by A5, XXREAL_0:1; then A6: i -' 1 = 0 by XREAL_1:232; A7: j <= width G by A3, MATRIX_1:38; right_cell (f,k,G) = cell (G,(i -' 1),j) by A1, A2, A3, A4, GOBRD13:28; then not (right_cell (f,k,G)) \ (L~ f) is bounded by A7, A6, JORDAN1B:33, TOPREAL6:90; then not RightComp f is bounded by A1, A2, JORDAN9:27, RLTOPSP1:42; then not BDD (L~ f) is bounded by GOBRD14:37; hence contradiction by JORDAN2C:106; ::_thesis: verum end; theorem Th17: :: JORDAN1I:17 for f being non constant standard clockwise_oriented special_circular_sequence for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds (f /. k) `2 <> N-bound (L~ f) proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds (f /. k) `2 <> N-bound (L~ f) let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds (f /. k) `2 <> N-bound (L~ f) ) assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) holds (f /. k) `2 <> N-bound (L~ f) let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) implies (f /. k) `2 <> N-bound (L~ f) ) assume that A2: ( 1 <= k & k + 1 <= len f ) and A3: [i,j] in Indices G and A4: [(i + 1),j] in Indices G and A5: f /. k = G * ((i + 1),j) and A6: f /. (k + 1) = G * (i,j) and A7: (f /. k) `2 = N-bound (L~ f) ; ::_thesis: contradiction A8: right_cell (f,k,G) = cell (G,i,j) by A1, A2, A3, A4, A5, A6, GOBRD13:26; A9: j <= width G by A4, MATRIX_1:38; A10: ( 1 <= i + 1 & 1 <= j ) by A4, MATRIX_1:38; set p = (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))); A11: ( 0 + 1 <= i & 1 <= j ) by A3, MATRIX_1:38; A12: j <= width G by A3, MATRIX_1:38; A13: i + 1 <= len G by A4, MATRIX_1:38; percases ( j = width G or j < width G ) by A12, XXREAL_0:1; suppose j = width G ; ::_thesis: contradiction hence contradiction by A1, A2, A3, A4, A5, A6, Th13; ::_thesis: verum end; supposeA14: j < width G ; ::_thesis: contradiction i < len G by A13, NAT_1:13; then A15: Int (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 A11, A14, GOBOARD6:26; j + 1 <= width G by A14, NAT_1:13; then A16: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in Int (right_cell (f,k,G)) by A11, A13, A8, GOBOARD6:31; then consider r, s being Real such that A17: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) = |[r,s]| and (G * (i,1)) `1 < r and r < (G * ((i + 1),1)) `1 and A18: (G * (1,j)) `2 < s and s < (G * (1,(j + 1))) `2 by A8, A15; ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `2 = s by A17, EUCLID:52; then ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `2 > N-bound (L~ f) by A5, A7, A13, A10, A9, A18, GOBOARD5:1; then A19: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in LeftComp f by Th12; Int (right_cell (f,k,G)) c= RightComp f by A1, A2, JORDAN1H:25; then (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in (LeftComp f) /\ (RightComp f) by A16, A19, XBOOLE_0:def_4; then LeftComp f meets RightComp f by XBOOLE_0:def_7; hence contradiction by GOBRD14:14; ::_thesis: verum end; end; end; theorem Th18: :: JORDAN1I:18 for f being non constant standard clockwise_oriented special_circular_sequence for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds (f /. k) `1 <> E-bound (L~ f) proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds (f /. k) `1 <> E-bound (L~ f) let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds (f /. k) `1 <> E-bound (L~ f) ) assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds (f /. k) `1 <> E-bound (L~ f) let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) implies (f /. k) `1 <> E-bound (L~ f) ) assume that A2: ( 1 <= k & k + 1 <= len f ) and A3: [i,j] in Indices G and A4: [i,(j + 1)] in Indices G and A5: f /. k = G * (i,j) and A6: f /. (k + 1) = G * (i,(j + 1)) and A7: (f /. k) `1 = E-bound (L~ f) ; ::_thesis: contradiction A8: right_cell (f,k,G) = cell (G,i,j) by A1, A2, A3, A4, A5, A6, GOBRD13:22; A9: j <= width G by A3, MATRIX_1:38; A10: ( 0 + 1 <= i & 1 <= j ) by A3, MATRIX_1:38; set p = (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))); A11: i <= len G by A3, MATRIX_1:38; A12: j + 1 <= width G by A4, MATRIX_1:38; percases ( i = len G or i < len G ) by A11, XXREAL_0:1; suppose i = len G ; ::_thesis: contradiction hence contradiction by A1, A2, A3, A4, A5, A6, Th14; ::_thesis: verum end; supposeA13: i < len G ; ::_thesis: contradiction j < width G by A12, NAT_1:13; then A14: Int (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 A10, A13, GOBOARD6:26; i + 1 <= len G by A13, NAT_1:13; then A15: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in Int (right_cell (f,k,G)) by A10, A12, A8, GOBOARD6:31; then consider r, s being Real such that A16: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) = |[r,s]| and A17: (G * (i,1)) `1 < r and r < (G * ((i + 1),1)) `1 and (G * (1,j)) `2 < s and s < (G * (1,(j + 1))) `2 by A8, A14; ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `1 = r by A16, EUCLID:52; then ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `1 > E-bound (L~ f) by A5, A7, A11, A10, A9, A17, GOBOARD5:2; then A18: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in LeftComp f by Th10; Int (right_cell (f,k,G)) c= RightComp f by A1, A2, JORDAN1H:25; then (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in (LeftComp f) /\ (RightComp f) by A15, A18, XBOOLE_0:def_4; then LeftComp f meets RightComp f by XBOOLE_0:def_7; hence contradiction by GOBRD14:14; ::_thesis: verum end; end; end; theorem Th19: :: JORDAN1I:19 for f being non constant standard clockwise_oriented special_circular_sequence for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds (f /. k) `2 <> S-bound (L~ f) proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds (f /. k) `2 <> S-bound (L~ f) let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds (f /. k) `2 <> S-bound (L~ f) ) assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds (f /. k) `2 <> S-bound (L~ f) let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) implies (f /. k) `2 <> S-bound (L~ f) ) assume that A2: ( 1 <= k & k + 1 <= len f ) and A3: [i,j] in Indices G and A4: [(i + 1),j] in Indices G and A5: f /. k = G * (i,j) and A6: f /. (k + 1) = G * ((i + 1),j) and A7: (f /. k) `2 = S-bound (L~ f) ; ::_thesis: contradiction A8: right_cell (f,k,G) = cell (G,i,(j -' 1)) by A1, A2, A3, A4, A5, A6, GOBRD13:24; A9: i <= len G by A3, MATRIX_1:38; A10: j <= width G by A3, MATRIX_1:38; A11: i + 1 <= len G by A4, MATRIX_1:38; set p = (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))); A12: 0 + 1 <= i by A3, MATRIX_1:38; A13: 1 <= j by A3, MATRIX_1:38; then A14: (j -' 1) + 1 = j by XREAL_1:235; percases ( j = 1 or j > 1 ) by A13, XXREAL_0:1; suppose j = 1 ; ::_thesis: contradiction hence contradiction by A1, A2, A3, A4, A5, A6, Th15; ::_thesis: verum end; suppose j > 1 ; ::_thesis: contradiction then j >= 1 + 1 by NAT_1:13; then A15: j - 1 >= (1 + 1) - 1 by XREAL_1:9; j < (width G) + 1 by A10, NAT_1:13; then A16: j - 1 < ((width G) + 1) - 1 by XREAL_1:9; i < len G by A11, NAT_1:13; then A17: Int (cell (G,i,(j -' 1))) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,(j -' 1))) `2 < s & s < (G * (1,j)) `2 ) } by A12, A14, A15, A16, GOBOARD6:26; A18: (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))) in Int (right_cell (f,k,G)) by A12, A10, A11, A8, A14, A15, GOBOARD6:31; then consider r, s being Real such that A19: (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))) = |[r,s]| and (G * (i,1)) `1 < r and r < (G * ((i + 1),1)) `1 and (G * (1,(j -' 1))) `2 < s and A20: s < (G * (1,j)) `2 by A8, A17; ((1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j)))) `2 = s by A19, EUCLID:52; then ((1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j)))) `2 < S-bound (L~ f) by A5, A7, A12, A9, A13, A10, A20, GOBOARD5:1; then A21: (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))) in LeftComp f by Th11; Int (right_cell (f,k,G)) c= RightComp f by A1, A2, JORDAN1H:25; then (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))) in (LeftComp f) /\ (RightComp f) by A18, A21, XBOOLE_0:def_4; then LeftComp f meets RightComp f by XBOOLE_0:def_7; hence contradiction by GOBRD14:14; ::_thesis: verum end; end; end; theorem Th20: :: JORDAN1I:20 for f being non constant standard clockwise_oriented special_circular_sequence for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds (f /. k) `1 <> W-bound (L~ f) proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board st f is_sequence_on G holds for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds (f /. k) `1 <> W-bound (L~ f) let G be Go-board; ::_thesis: ( f is_sequence_on G implies for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds (f /. k) `1 <> W-bound (L~ f) ) assume A1: f is_sequence_on G ; ::_thesis: for i, j, k being Element of NAT st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds (f /. k) `1 <> W-bound (L~ f) let i, j, k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) implies (f /. k) `1 <> W-bound (L~ f) ) assume that A2: ( 1 <= k & k + 1 <= len f ) and A3: [i,j] in Indices G and A4: [i,(j + 1)] in Indices G and A5: f /. k = G * (i,(j + 1)) and A6: f /. (k + 1) = G * (i,j) and A7: (f /. k) `1 = W-bound (L~ f) ; ::_thesis: contradiction A8: right_cell (f,k,G) = cell (G,(i -' 1),j) by A1, A2, A3, A4, A5, A6, GOBRD13:28; A9: ( 1 <= i & i <= len G ) by A4, MATRIX_1:38; A10: 1 <= j by A3, MATRIX_1:38; A11: 1 <= j + 1 by A4, MATRIX_1:38; A12: j + 1 <= width G by A4, MATRIX_1:38; set p = (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))); A13: i <= len G by A3, MATRIX_1:38; A14: 0 + 1 <= i by A3, MATRIX_1:38; then A15: (i -' 1) + 1 = i by XREAL_1:235; percases ( i = 1 or i > 1 ) by A14, XXREAL_0:1; suppose i = 1 ; ::_thesis: contradiction hence contradiction by A1, A2, A3, A4, A5, A6, Th16; ::_thesis: verum end; suppose i > 1 ; ::_thesis: contradiction then i >= 1 + 1 by NAT_1:13; then A16: i - 1 >= (1 + 1) - 1 by XREAL_1:9; i < (len G) + 1 by A13, NAT_1:13; then A17: i - 1 < ((len G) + 1) - 1 by XREAL_1:9; j < width G by A12, NAT_1:13; then A18: Int (cell (G,(i -' 1),j)) = { |[r,s]| where r, s is Real : ( (G * ((i -' 1),1)) `1 < r & r < (G * (i,1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } by A10, A15, A16, A17, GOBOARD6:26; A19: (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in Int (right_cell (f,k,G)) by A13, A10, A12, A8, A15, A16, GOBOARD6:31; then consider r, s being Real such that A20: (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) = |[r,s]| and (G * ((i -' 1),1)) `1 < r and A21: r < (G * (i,1)) `1 and (G * (1,j)) `2 < s and s < (G * (1,(j + 1))) `2 by A8, A18; ((1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))))) `1 = r by A20, EUCLID:52; then ((1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))))) `1 < W-bound (L~ f) by A5, A7, A9, A11, A12, A21, GOBOARD5:2; then A22: (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in LeftComp f by Th9; Int (right_cell (f,k,G)) c= RightComp f by A1, A2, JORDAN1H:25; then (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in (LeftComp f) /\ (RightComp f) by A19, A22, XBOOLE_0:def_4; then LeftComp f meets RightComp f by XBOOLE_0:def_7; hence contradiction by GOBRD14:14; ::_thesis: verum end; end; end; theorem Th21: :: JORDAN1I:21 for f being non constant standard clockwise_oriented special_circular_sequence for G being Go-board for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = W-min (L~ f) holds ex i, j being Element of NAT st ( [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) ) proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = W-min (L~ f) holds ex i, j being Element of NAT st ( [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) ) let G be Go-board; ::_thesis: for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = W-min (L~ f) holds ex i, j being Element of NAT st ( [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) ) let k be Element of NAT ; ::_thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = W-min (L~ f) implies ex i, j being Element of NAT st ( [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) ) ) assume that A1: f is_sequence_on G and A2: 1 <= k and A3: k + 1 <= len f and A4: f /. k = W-min (L~ f) ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) ) consider i1, j1, i2, j2 being Element of NAT such that A5: [i1,j1] in Indices G and A6: f /. k = G * (i1,j1) and A7: [i2,j2] in Indices G and A8: f /. (k + 1) = G * (i2,j2) and A9: ( ( 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, A2, A3, JORDAN8:3; A10: (G * (i1,j1)) `1 = W-bound (L~ f) by A4, A6, EUCLID:52; A11: 1 <= j2 by A7, MATRIX_1:38; A12: 1 <= i2 by A7, MATRIX_1:38; take i1 ; ::_thesis: ex j being Element of NAT st ( [i1,j] in Indices G & [i1,(j + 1)] in Indices G & f /. k = G * (i1,j) & f /. (k + 1) = G * (i1,(j + 1)) ) take j1 ; ::_thesis: ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) A13: 1 <= i1 by A5, MATRIX_1:38; A14: k + 1 >= 1 + 1 by A2, XREAL_1:7; then A15: len f >= 2 by A3, XXREAL_0:2; k + 1 >= 1 by NAT_1:11; then A16: k + 1 in dom f by A3, FINSEQ_3:25; then f /. (k + 1) in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2; then A17: (G * (i1,j1)) `1 <= (G * (i2,j2)) `1 by A8, A10, PSCOMP_1:24; A18: ( i1 <= len G & j1 <= width G ) by A5, MATRIX_1:38; A19: k < len f by A3, NAT_1:13; then A20: k in dom f by A2, FINSEQ_3:25; A21: ( i2 <= len G & j2 <= width G ) by A7, MATRIX_1:38; A22: 1 <= j1 by A5, MATRIX_1:38; percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 & k <> 1 ) or ( i1 + 1 = i2 & j1 = j2 & k = 1 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A9; supposeA23: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) thus [i1,j1] in Indices G by A5; ::_thesis: ( [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) thus [i1,(j1 + 1)] in Indices G by A7, A23; ::_thesis: ( f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) thus f /. k = G * (i1,j1) by A6; ::_thesis: f /. (k + 1) = G * (i1,(j1 + 1)) thus f /. (k + 1) = G * (i1,(j1 + 1)) by A8, A23; ::_thesis: verum end; supposeA24: ( i1 + 1 = i2 & j1 = j2 & k <> 1 ) ; ::_thesis: ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) reconsider k9 = k - 1 as Element of NAT by A20, FINSEQ_3:26; k > 1 by A2, A24, XXREAL_0:1; then k >= 1 + 1 by NAT_1:13; then A25: k9 >= (1 + 1) - 1 by XREAL_1:9; then consider i3, j3, i4, j4 being Element of NAT such that A26: [i3,j3] in Indices G and A27: f /. k9 = G * (i3,j3) and A28: [i4,j4] in Indices G and A29: f /. (k9 + 1) = G * (i4,j4) and A30: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A19, JORDAN8:3; A31: i1 = i4 by A5, A6, A28, A29, GOBOARD1:5; k9 + 1 < len f by A3, NAT_1:13; then k9 < len f by NAT_1:13; then A32: k9 in dom f by A25, FINSEQ_3:25; A33: 1 <= i3 by A26, MATRIX_1:38; A34: j1 = j4 by A5, A6, A28, A29, GOBOARD1:5; A35: 1 <= j3 by A26, MATRIX_1:38; A36: ( i3 <= len G & j3 <= width G ) by A26, MATRIX_1:38; A37: j3 = j4 proof assume A38: j3 <> j4 ; ::_thesis: contradiction percases ( ( i3 = i4 & j3 = j4 + 1 ) or ( i3 = i4 & j3 + 1 = j4 ) ) by A30, A38; supposeA39: ( i3 = i4 & j3 = j4 + 1 ) ; ::_thesis: contradiction then (G * (i3,j3)) `1 <> W-bound (L~ f) by A1, A19, A25, A26, A27, A28, A29, Th20; then (G * (i3,1)) `1 <> W-bound (L~ f) by A33, A35, A36, GOBOARD5:2; then (W-min (L~ f)) `1 <> W-bound (L~ f) by A4, A6, A13, A22, A18, A31, A39, GOBOARD5:2; hence contradiction by EUCLID:52; ::_thesis: verum end; supposeA40: ( i3 = i4 & j3 + 1 = j4 ) ; ::_thesis: contradiction (G * (i3,j3)) `1 = (G * (i3,1)) `1 by A33, A35, A36, GOBOARD5:2 .= (W-min (L~ f)) `1 by A4, A6, A13, A22, A18, A31, A40, GOBOARD5:2 .= W-bound (L~ f) by EUCLID:52 ; then G * (i3,j3) in W-most (L~ f) by A15, A27, A32, GOBOARD1:1, SPRECT_2:12; then (G * (i4,j4)) `2 <= (G * (i3,j3)) `2 by A4, A29, PSCOMP_1:31; then j3 >= j3 + 1 by A13, A18, A31, A34, A35, A40, GOBOARD5:4; hence contradiction by NAT_1:13; ::_thesis: verum end; end; end; A41: k9 + 1 = k ; f /. k9 in L~ f by A3, A14, A32, GOBOARD1:1, XXREAL_0:2; then A42: (G * (i1,j1)) `1 <= (G * (i3,j3)) `1 by A10, A27, PSCOMP_1:24; now__::_thesis:_contradiction percases ( i3 + 1 = i4 or i3 = i4 + 1 ) by A30, A37; suppose i3 + 1 = i4 ; ::_thesis: contradiction then i3 >= i3 + 1 by A22, A18, A31, A34, A33, A42, A37, GOBOARD5:3; hence contradiction by NAT_1:13; ::_thesis: verum end; supposeA43: i3 = i4 + 1 ; ::_thesis: contradiction k9 + (1 + 1) <= len f by A3; then A44: (LSeg (f,k9)) /\ (LSeg (f,k)) = {(f /. k)} by A25, A41, TOPREAL1:def_6; ( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A19, A25, A41, TOPREAL1:21; then f /. (k + 1) in {(f /. k)} by A8, A24, A27, A31, A34, A37, A43, A44, XBOOLE_0:def_4; then A45: f /. (k + 1) = f /. k by TARSKI:def_1; i1 <> i2 by A24; hence contradiction by A5, A6, A7, A8, A45, GOBOARD1:5; ::_thesis: verum end; end; end; hence ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) ; ::_thesis: verum end; supposeA46: ( i1 + 1 = i2 & j1 = j2 & k = 1 ) ; ::_thesis: ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) set k1 = len f; k < len f by A3, NAT_1:13; then A47: len f > 1 + 0 by A2, XXREAL_0:2; then len f in dom f by FINSEQ_3:25; then reconsider k9 = (len f) - 1 as Element of NAT by FINSEQ_3:26; k + 1 >= 1 + 1 by A2, XREAL_1:7; then len f >= 1 + 1 by A3, XXREAL_0:2; then A48: k9 >= (1 + 1) - 1 by XREAL_1:9; then consider i3, j3, i4, j4 being Element of NAT such that A49: [i3,j3] in Indices G and A50: f /. k9 = G * (i3,j3) and A51: [i4,j4] in Indices G and A52: f /. (k9 + 1) = G * (i4,j4) and A53: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, JORDAN8:3; A54: f /. (len f) = f /. 1 by FINSEQ_6:def_1; then A55: i1 = i4 by A5, A6, A46, A51, A52, GOBOARD1:5; A56: j1 = j4 by A5, A6, A46, A54, A51, A52, GOBOARD1:5; A57: 1 <= j3 by A49, MATRIX_1:38; k9 + 1 <= len f ; then k9 < len f by NAT_1:13; then A58: k9 in dom f by A48, FINSEQ_3:25; then f /. k9 in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2; then A59: (G * (i1,j1)) `1 <= (G * (i3,j3)) `1 by A10, A50, PSCOMP_1:24; A60: 1 <= i3 by A49, MATRIX_1:38; A61: ( i3 <= len G & j3 <= width G ) by A49, MATRIX_1:38; A62: j3 = j4 proof assume A63: j3 <> j4 ; ::_thesis: contradiction percases ( ( i3 = i4 & j3 = j4 + 1 ) or ( i3 = i4 & j3 + 1 = j4 ) ) by A53, A63; supposeA64: ( i3 = i4 & j3 = j4 + 1 ) ; ::_thesis: contradiction then (G * (i3,j3)) `1 <> W-bound (L~ f) by A1, A48, A49, A50, A51, A52, Th20; then (G * (i3,1)) `1 <> W-bound (L~ f) by A60, A57, A61, GOBOARD5:2; then (W-min (L~ f)) `1 <> W-bound (L~ f) by A4, A6, A13, A22, A18, A55, A64, GOBOARD5:2; hence contradiction by EUCLID:52; ::_thesis: verum end; supposeA65: ( i3 = i4 & j3 + 1 = j4 ) ; ::_thesis: contradiction (G * (i3,j3)) `1 = (G * (i3,1)) `1 by A60, A57, A61, GOBOARD5:2 .= (W-min (L~ f)) `1 by A4, A6, A13, A22, A18, A55, A65, GOBOARD5:2 .= W-bound (L~ f) by EUCLID:52 ; then G * (i3,j3) in W-most (L~ f) by A15, A50, A58, GOBOARD1:1, SPRECT_2:12; then (G * (i4,j4)) `2 <= (G * (i3,j3)) `2 by A4, A46, A54, A52, PSCOMP_1:31; then j3 >= j3 + 1 by A13, A18, A55, A56, A57, A65, GOBOARD5:4; hence contradiction by NAT_1:13; ::_thesis: verum end; end; end; A66: k9 + 1 = len f ; now__::_thesis:_contradiction percases ( i3 + 1 = i4 or i3 = i4 + 1 ) by A53, A62; suppose i3 + 1 = i4 ; ::_thesis: contradiction then i3 >= i3 + 1 by A22, A18, A55, A56, A60, A59, A62, GOBOARD5:3; hence contradiction by NAT_1:13; ::_thesis: verum end; supposeA67: i3 = i4 + 1 ; ::_thesis: contradiction (len f) - 1 >= 0 by A47, XREAL_1:19; then (len f) -' 1 = (len f) - 1 by XREAL_0:def_2; then A68: (LSeg (f,k)) /\ (LSeg (f,k9)) = {(f . k)} by A46, JORDAN4:42 .= {(f /. k)} by A20, PARTFUN1:def_6 ; ( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A48, A66, TOPREAL1:21; then f /. (k + 1) in {(f /. k)} by A8, A46, A50, A55, A56, A62, A67, A68, XBOOLE_0:def_4; then A69: f /. (k + 1) = f /. k by TARSKI:def_1; i1 <> i2 by A46; hence contradiction by A5, A6, A7, A8, A69, GOBOARD1:5; ::_thesis: verum end; end; end; hence ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) ; ::_thesis: verum end; suppose ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) then i2 >= i2 + 1 by A22, A18, A12, A17, GOBOARD5:3; hence ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) by NAT_1:13; ::_thesis: verum end; supposeA70: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) (G * (i2,j2)) `1 = (G * (i2,1)) `1 by A12, A11, A21, GOBOARD5:2 .= W-bound (L~ f) by A13, A22, A18, A10, A70, GOBOARD5:2 ; then G * (i2,j2) in W-most (L~ f) by A8, A15, A16, GOBOARD1:1, SPRECT_2:12; then (G * (i1,j1)) `2 <= (G * (i2,j2)) `2 by A4, A6, PSCOMP_1:31; then j2 >= j2 + 1 by A13, A18, A11, A70, GOBOARD5:4; hence ( [i1,j1] in Indices G & [i1,(j1 + 1)] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * (i1,(j1 + 1)) ) by NAT_1:13; ::_thesis: verum end; end; end; theorem :: JORDAN1I:22 for f being non constant standard clockwise_oriented special_circular_sequence for G being Go-board for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) holds ex i, j being Element of NAT st ( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) ) proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) holds ex i, j being Element of NAT st ( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) ) let G be Go-board; ::_thesis: for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) holds ex i, j being Element of NAT st ( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) ) let k be Element of NAT ; ::_thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = N-min (L~ f) implies ex i, j being Element of NAT st ( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) ) ) assume that A1: f is_sequence_on G and A2: 1 <= k and A3: k + 1 <= len f and A4: f /. k = N-min (L~ f) ; ::_thesis: ex i, j being Element of NAT st ( [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) ) consider i1, j1, i2, j2 being Element of NAT such that A5: [i1,j1] in Indices G and A6: f /. k = G * (i1,j1) and A7: [i2,j2] in Indices G and A8: f /. (k + 1) = G * (i2,j2) and A9: ( ( 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, A2, A3, JORDAN8:3; A10: (G * (i1,j1)) `2 = N-bound (L~ f) by A4, A6, EUCLID:52; A11: j2 <= width G by A7, MATRIX_1:38; A12: 1 <= i2 by A7, MATRIX_1:38; take i1 ; ::_thesis: ex j being Element of NAT st ( [i1,j] in Indices G & [(i1 + 1),j] in Indices G & f /. k = G * (i1,j) & f /. (k + 1) = G * ((i1 + 1),j) ) take j1 ; ::_thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) A13: 1 <= i1 by A5, MATRIX_1:38; A14: k + 1 >= 1 + 1 by A2, XREAL_1:7; then A15: len f >= 2 by A3, XXREAL_0:2; k + 1 >= 1 by NAT_1:11; then A16: k + 1 in dom f by A3, FINSEQ_3:25; then f /. (k + 1) in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2; then A17: (G * (i1,j1)) `2 >= (G * (i2,j2)) `2 by A8, A10, PSCOMP_1:24; A18: j1 <= width G by A5, MATRIX_1:38; A19: k < len f by A3, NAT_1:13; then A20: k in dom f by A2, FINSEQ_3:25; A21: ( i2 <= len G & 1 <= j2 ) by A7, MATRIX_1:38; A22: ( i1 <= len G & 1 <= j1 ) by A5, MATRIX_1:38; percases ( ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 & j2 + 1 = j1 & k <> 1 ) or ( i1 = i2 & j2 + 1 = j1 & k = 1 ) or ( i1 = i2 & j2 = j1 + 1 ) or ( i1 = i2 + 1 & j1 = j2 ) ) by A9; supposeA23: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) thus [i1,j1] in Indices G by A5; ::_thesis: ( [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) thus [(i1 + 1),j1] in Indices G by A7, A23; ::_thesis: ( f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) thus f /. k = G * (i1,j1) by A6; ::_thesis: f /. (k + 1) = G * ((i1 + 1),j1) thus f /. (k + 1) = G * ((i1 + 1),j1) by A8, A23; ::_thesis: verum end; supposeA24: ( i1 = i2 & j2 + 1 = j1 & k <> 1 ) ; ::_thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) reconsider k9 = k - 1 as Element of NAT by A20, FINSEQ_3:26; k > 1 by A2, A24, XXREAL_0:1; then k >= 1 + 1 by NAT_1:13; then A25: k9 >= (1 + 1) - 1 by XREAL_1:9; then consider i3, j3, i4, j4 being Element of NAT such that A26: [i3,j3] in Indices G and A27: f /. k9 = G * (i3,j3) and A28: [i4,j4] in Indices G and A29: f /. (k9 + 1) = G * (i4,j4) and A30: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A19, JORDAN8:3; A31: i1 = i4 by A5, A6, A28, A29, GOBOARD1:5; k9 + 1 < len f by A3, NAT_1:13; then k9 < len f by NAT_1:13; then A32: k9 in dom f by A25, FINSEQ_3:25; A33: 1 <= i3 by A26, MATRIX_1:38; A34: j3 <= width G by A26, MATRIX_1:38; A35: j1 = j4 by A5, A6, A28, A29, GOBOARD1:5; A36: ( i3 <= len G & 1 <= j3 ) by A26, MATRIX_1:38; A37: i3 = i4 proof assume A38: i3 <> i4 ; ::_thesis: contradiction percases ( ( j3 = j4 & i3 = i4 + 1 ) or ( j3 = j4 & i3 + 1 = i4 ) ) by A30, A38; supposeA39: ( j3 = j4 & i3 = i4 + 1 ) ; ::_thesis: contradiction then (G * (i3,j3)) `2 <> N-bound (L~ f) by A1, A19, A25, A26, A27, A28, A29, Th17; then (G * (1,j3)) `2 <> N-bound (L~ f) by A33, A36, A34, GOBOARD5:1; then (N-min (L~ f)) `2 <> N-bound (L~ f) by A4, A6, A13, A22, A18, A35, A39, GOBOARD5:1; hence contradiction by EUCLID:52; ::_thesis: verum end; supposeA40: ( j3 = j4 & i3 + 1 = i4 ) ; ::_thesis: contradiction (G * (i3,j3)) `2 = (G * (1,j3)) `2 by A33, A36, A34, GOBOARD5:1 .= (N-min (L~ f)) `2 by A4, A6, A13, A22, A18, A35, A40, GOBOARD5:1 .= N-bound (L~ f) by EUCLID:52 ; then G * (i3,j3) in N-most (L~ f) by A15, A27, A32, GOBOARD1:1, SPRECT_2:10; then (G * (i4,j4)) `1 <= (G * (i3,j3)) `1 by A4, A29, PSCOMP_1:39; then i3 >= i3 + 1 by A22, A18, A31, A35, A33, A40, GOBOARD5:3; hence contradiction by NAT_1:13; ::_thesis: verum end; end; end; A41: k9 + 1 = k ; f /. k9 in L~ f by A3, A14, A32, GOBOARD1:1, XXREAL_0:2; then A42: (G * (i1,j1)) `2 >= (G * (i3,j3)) `2 by A10, A27, PSCOMP_1:24; now__::_thesis:_contradiction percases ( j4 + 1 = j3 or j4 = j3 + 1 ) by A30, A37; suppose j4 + 1 = j3 ; ::_thesis: contradiction then j4 >= j4 + 1 by A13, A22, A31, A35, A34, A42, A37, GOBOARD5:4; hence contradiction by NAT_1:13; ::_thesis: verum end; supposeA43: j4 = j3 + 1 ; ::_thesis: contradiction k9 + (1 + 1) <= len f by A3; then A44: (LSeg (f,k9)) /\ (LSeg (f,k)) = {(f /. k)} by A25, A41, TOPREAL1:def_6; ( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A19, A25, A41, TOPREAL1:21; then f /. (k + 1) in {(f /. k)} by A8, A24, A27, A31, A35, A37, A43, A44, XBOOLE_0:def_4; then A45: f /. (k + 1) = f /. k by TARSKI:def_1; j1 <> j2 by A24; hence contradiction by A5, A6, A7, A8, A45, GOBOARD1:5; ::_thesis: verum end; end; end; hence ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) ; ::_thesis: verum end; supposeA46: ( i1 = i2 & j2 + 1 = j1 & k = 1 ) ; ::_thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) set k1 = len f; k < len f by A3, NAT_1:13; then A47: len f > 1 + 0 by A2, XXREAL_0:2; then len f in dom f by FINSEQ_3:25; then reconsider k9 = (len f) - 1 as Element of NAT by FINSEQ_3:26; k + 1 >= 1 + 1 by A2, XREAL_1:7; then len f >= 1 + 1 by A3, XXREAL_0:2; then A48: k9 >= (1 + 1) - 1 by XREAL_1:9; then consider i3, j3, i4, j4 being Element of NAT such that A49: [i3,j3] in Indices G and A50: f /. k9 = G * (i3,j3) and A51: [i4,j4] in Indices G and A52: f /. (k9 + 1) = G * (i4,j4) and A53: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, JORDAN8:3; A54: f /. (len f) = f /. 1 by FINSEQ_6:def_1; then A55: i1 = i4 by A5, A6, A46, A51, A52, GOBOARD1:5; k9 + 1 <= len f ; then k9 < len f by NAT_1:13; then A56: k9 in dom f by A48, FINSEQ_3:25; then f /. k9 in L~ f by A3, A14, GOBOARD1:1, XXREAL_0:2; then A57: (G * (i1,j1)) `2 >= (G * (i3,j3)) `2 by A10, A50, PSCOMP_1:24; A58: 1 <= i3 by A49, MATRIX_1:38; A59: j1 = j4 by A5, A6, A46, A54, A51, A52, GOBOARD1:5; A60: j3 <= width G by A49, MATRIX_1:38; A61: ( i3 <= len G & 1 <= j3 ) by A49, MATRIX_1:38; A62: i3 = i4 proof assume A63: i3 <> i4 ; ::_thesis: contradiction percases ( ( j3 = j4 & i3 = i4 + 1 ) or ( j3 = j4 & i3 + 1 = i4 ) ) by A53, A63; supposeA64: ( j3 = j4 & i3 = i4 + 1 ) ; ::_thesis: contradiction then (G * (i3,j3)) `2 <> N-bound (L~ f) by A1, A48, A49, A50, A51, A52, Th17; then (G * (1,j3)) `2 <> N-bound (L~ f) by A58, A61, A60, GOBOARD5:1; then (N-min (L~ f)) `2 <> N-bound (L~ f) by A4, A6, A13, A22, A18, A59, A64, GOBOARD5:1; hence contradiction by EUCLID:52; ::_thesis: verum end; supposeA65: ( j3 = j4 & i3 + 1 = i4 ) ; ::_thesis: contradiction (G * (i3,j3)) `2 = (G * (1,j3)) `2 by A58, A61, A60, GOBOARD5:1 .= (N-min (L~ f)) `2 by A4, A6, A13, A22, A18, A59, A65, GOBOARD5:1 .= N-bound (L~ f) by EUCLID:52 ; then G * (i3,j3) in N-most (L~ f) by A15, A50, A56, GOBOARD1:1, SPRECT_2:10; then (G * (i4,j4)) `1 <= (G * (i3,j3)) `1 by A4, A46, A54, A52, PSCOMP_1:39; then i3 >= i3 + 1 by A22, A18, A55, A59, A58, A65, GOBOARD5:3; hence contradiction by NAT_1:13; ::_thesis: verum end; end; end; A66: k9 + 1 = len f ; now__::_thesis:_contradiction percases ( j4 + 1 = j3 or j4 = j3 + 1 ) by A53, A62; suppose j4 + 1 = j3 ; ::_thesis: contradiction then j4 >= j4 + 1 by A13, A22, A55, A59, A60, A57, A62, GOBOARD5:4; hence contradiction by NAT_1:13; ::_thesis: verum end; supposeA67: j4 = j3 + 1 ; ::_thesis: contradiction (len f) - 1 >= 0 by A47, XREAL_1:19; then (len f) -' 1 = (len f) - 1 by XREAL_0:def_2; then A68: (LSeg (f,k)) /\ (LSeg (f,k9)) = {(f . k)} by A46, JORDAN4:42 .= {(f /. k)} by A20, PARTFUN1:def_6 ; ( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A48, A66, TOPREAL1:21; then f /. (k + 1) in {(f /. k)} by A8, A46, A50, A55, A59, A62, A67, A68, XBOOLE_0:def_4; then A69: f /. (k + 1) = f /. k by TARSKI:def_1; j1 <> j2 by A46; hence contradiction by A5, A6, A7, A8, A69, GOBOARD1:5; ::_thesis: verum end; end; end; hence ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) ; ::_thesis: verum end; suppose ( i1 = i2 & j2 = j1 + 1 ) ; ::_thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) then j1 >= j1 + 1 by A13, A22, A11, A17, GOBOARD5:4; hence ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) by NAT_1:13; ::_thesis: verum end; supposeA70: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) (G * (i2,j2)) `2 = (G * (1,j2)) `2 by A12, A21, A11, GOBOARD5:1 .= N-bound (L~ f) by A13, A22, A18, A10, A70, GOBOARD5:1 ; then G * (i2,j2) in N-most (L~ f) by A8, A15, A16, GOBOARD1:1, SPRECT_2:10; then (G * (i1,j1)) `1 <= (G * (i2,j2)) `1 by A4, A6, PSCOMP_1:39; then i2 >= i2 + 1 by A22, A18, A12, A70, GOBOARD5:3; hence ( [i1,j1] in Indices G & [(i1 + 1),j1] in Indices G & f /. k = G * (i1,j1) & f /. (k + 1) = G * ((i1 + 1),j1) ) by NAT_1:13; ::_thesis: verum end; end; end; theorem Th23: :: JORDAN1I:23 for f being non constant standard clockwise_oriented special_circular_sequence for G being Go-board for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) holds ex i, j being Element of NAT st ( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) ) proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) holds ex i, j being Element of NAT st ( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) ) let G be Go-board; ::_thesis: for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) holds ex i, j being Element of NAT st ( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) ) let k be Element of NAT ; ::_thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = E-max (L~ f) implies ex i, j being Element of NAT st ( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) ) ) assume that A1: f is_sequence_on G and A2: 1 <= k and A3: k + 1 <= len f and A4: f /. k = E-max (L~ f) ; ::_thesis: ex i, j being Element of NAT st ( [i,(j + 1)] in Indices G & [i,j] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) ) consider i1, j1, i2, j2 being Element of NAT such that A5: [i1,j1] in Indices G and A6: f /. k = G * (i1,j1) and A7: [i2,j2] in Indices G and A8: f /. (k + 1) = G * (i2,j2) and A9: ( ( 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, A2, A3, JORDAN8:3; A10: (G * (i1,j1)) `1 = E-bound (L~ f) by A4, A6, EUCLID:52; A11: j2 <= width G by A7, MATRIX_1:38; take i2 ; ::_thesis: ex j being Element of NAT st ( [i2,(j + 1)] in Indices G & [i2,j] in Indices G & f /. k = G * (i2,(j + 1)) & f /. (k + 1) = G * (i2,j) ) take j2 ; ::_thesis: ( [i2,(j2 + 1)] in Indices G & [i2,j2] in Indices G & f /. k = G * (i2,(j2 + 1)) & f /. (k + 1) = G * (i2,j2) ) A12: i1 <= len G by A5, MATRIX_1:38; A13: k + 1 >= 1 + 1 by A2, XREAL_1:7; then A14: len f >= 2 by A3, XXREAL_0:2; k + 1 >= 1 by NAT_1:11; then A15: k + 1 in dom f by A3, FINSEQ_3:25; then f /. (k + 1) in L~ f by A3, A13, GOBOARD1:1, XXREAL_0:2; then A16: (G * (i1,j1)) `1 >= (G * (i2,j2)) `1 by A8, A10, PSCOMP_1:24; A17: ( 1 <= i1 & 1 <= j1 ) by A5, MATRIX_1:38; A18: k < len f by A3, NAT_1:13; then A19: k in dom f by A2, FINSEQ_3:25; A20: i2 <= len G by A7, MATRIX_1:38; A21: j1 <= width G by A5, MATRIX_1:38; A22: ( 1 <= i2 & 1 <= j2 ) by A7, MATRIX_1:38; now__::_thesis:_(_[i2,j2]_in_Indices_G_&_[i2,(j2_+_1)]_in_Indices_G_&_f_/._k_=_G_*_(i2,(j2_+_1))_) percases ( ( i1 = i2 & j2 + 1 = j1 ) or ( i2 + 1 = i1 & j2 = j1 & k <> 1 ) or ( i2 + 1 = i1 & j2 = j1 & k = 1 ) or ( i2 = i1 + 1 & j1 = j2 ) or ( i1 = i2 & j2 = j1 + 1 ) ) by A9; suppose ( i1 = i2 & j2 + 1 = j1 ) ; ::_thesis: ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) hence ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) by A5, A6, A7; ::_thesis: verum end; supposeA23: ( i2 + 1 = i1 & j2 = j1 & k <> 1 ) ; ::_thesis: ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) reconsider k9 = k - 1 as Element of NAT by A19, FINSEQ_3:26; k > 1 by A2, A23, XXREAL_0:1; then k >= 1 + 1 by NAT_1:13; then A24: k9 >= (1 + 1) - 1 by XREAL_1:9; then consider i3, j3, i4, j4 being Element of NAT such that A25: [i3,j3] in Indices G and A26: f /. k9 = G * (i3,j3) and A27: [i4,j4] in Indices G and A28: f /. (k9 + 1) = G * (i4,j4) and A29: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A18, JORDAN8:3; A30: i1 = i4 by A5, A6, A27, A28, GOBOARD1:5; k9 + 1 < len f by A3, NAT_1:13; then k9 < len f by NAT_1:13; then A31: k9 in dom f by A24, FINSEQ_3:25; A32: i3 <= len G by A25, MATRIX_1:38; A33: j1 = j4 by A5, A6, A27, A28, GOBOARD1:5; A34: j3 <= width G by A25, MATRIX_1:38; A35: ( 1 <= i3 & 1 <= j3 ) by A25, MATRIX_1:38; A36: j3 = j4 proof assume A37: j3 <> j4 ; ::_thesis: contradiction percases ( ( i3 = i4 & j4 = j3 + 1 ) or ( i3 = i4 & j4 + 1 = j3 ) ) by A29, A37; supposeA38: ( i3 = i4 & j4 = j3 + 1 ) ; ::_thesis: contradiction then (G * (i3,j3)) `1 <> E-bound (L~ f) by A1, A18, A24, A25, A26, A27, A28, Th18; then (G * (i3,1)) `1 <> E-bound (L~ f) by A32, A35, A34, GOBOARD5:2; then (E-max (L~ f)) `1 <> E-bound (L~ f) by A4, A6, A12, A17, A21, A30, A38, GOBOARD5:2; hence contradiction by EUCLID:52; ::_thesis: verum end; supposeA39: ( i3 = i4 & j4 + 1 = j3 ) ; ::_thesis: contradiction (G * (i3,j3)) `1 = (G * (i3,1)) `1 by A32, A35, A34, GOBOARD5:2 .= (E-max (L~ f)) `1 by A4, A6, A12, A17, A21, A30, A39, GOBOARD5:2 .= E-bound (L~ f) by EUCLID:52 ; then G * (i3,j3) in E-most (L~ f) by A14, A26, A31, GOBOARD1:1, SPRECT_2:13; then (G * (i4,j4)) `2 >= (G * (i3,j3)) `2 by A4, A28, PSCOMP_1:47; then j4 >= j4 + 1 by A12, A17, A30, A33, A34, A39, GOBOARD5:4; hence contradiction by NAT_1:13; ::_thesis: verum end; end; end; A40: k9 + 1 = k ; f /. k9 in L~ f by A3, A13, A31, GOBOARD1:1, XXREAL_0:2; then A41: (G * (i1,j1)) `1 >= (G * (i3,j3)) `1 by A10, A26, PSCOMP_1:24; now__::_thesis:_contradiction percases ( i4 + 1 = i3 or i4 = i3 + 1 ) by A29, A36; suppose i4 + 1 = i3 ; ::_thesis: contradiction then i4 >= i4 + 1 by A17, A21, A30, A33, A32, A41, A36, GOBOARD5:3; hence contradiction by NAT_1:13; ::_thesis: verum end; supposeA42: i4 = i3 + 1 ; ::_thesis: contradiction k9 + (1 + 1) <= len f by A3; then A43: (LSeg (f,k9)) /\ (LSeg (f,k)) = {(f /. k)} by A24, A40, TOPREAL1:def_6; ( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A18, A24, A40, TOPREAL1:21; then f /. (k + 1) in {(f /. k)} by A8, A23, A26, A30, A33, A36, A42, A43, XBOOLE_0:def_4; then A44: f /. (k + 1) = f /. k by TARSKI:def_1; i1 <> i2 by A23; hence contradiction by A5, A6, A7, A8, A44, GOBOARD1:5; ::_thesis: verum end; end; end; hence ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) ; ::_thesis: verum end; supposeA45: ( i2 + 1 = i1 & j2 = j1 & k = 1 ) ; ::_thesis: ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) set k1 = len f; k < len f by A3, NAT_1:13; then A46: len f > 1 + 0 by A2, XXREAL_0:2; then len f in dom f by FINSEQ_3:25; then reconsider k9 = (len f) - 1 as Element of NAT by FINSEQ_3:26; k + 1 >= 1 + 1 by A2, XREAL_1:7; then len f >= 1 + 1 by A3, XXREAL_0:2; then A47: k9 >= (1 + 1) - 1 by XREAL_1:9; then consider i3, j3, i4, j4 being Element of NAT such that A48: [i3,j3] in Indices G and A49: f /. k9 = G * (i3,j3) and A50: [i4,j4] in Indices G and A51: f /. (k9 + 1) = G * (i4,j4) and A52: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, JORDAN8:3; A53: f /. (len f) = f /. 1 by FINSEQ_6:def_1; then A54: i1 = i4 by A5, A6, A45, A50, A51, GOBOARD1:5; A55: j1 = j4 by A5, A6, A45, A53, A50, A51, GOBOARD1:5; A56: j3 <= width G by A48, MATRIX_1:38; k9 + 1 <= len f ; then k9 < len f by NAT_1:13; then A57: k9 in dom f by A47, FINSEQ_3:25; then f /. k9 in L~ f by A3, A13, GOBOARD1:1, XXREAL_0:2; then A58: (G * (i1,j1)) `1 >= (G * (i3,j3)) `1 by A10, A49, PSCOMP_1:24; A59: i3 <= len G by A48, MATRIX_1:38; A60: ( 1 <= i3 & 1 <= j3 ) by A48, MATRIX_1:38; A61: j3 = j4 proof assume A62: j3 <> j4 ; ::_thesis: contradiction percases ( ( i3 = i4 & j4 = j3 + 1 ) or ( i3 = i4 & j4 + 1 = j3 ) ) by A52, A62; supposeA63: ( i3 = i4 & j4 = j3 + 1 ) ; ::_thesis: contradiction then (G * (i3,j3)) `1 <> E-bound (L~ f) by A1, A47, A48, A49, A50, A51, Th18; then (G * (i3,1)) `1 <> E-bound (L~ f) by A59, A60, A56, GOBOARD5:2; then (E-max (L~ f)) `1 <> E-bound (L~ f) by A4, A6, A12, A17, A21, A54, A63, GOBOARD5:2; hence contradiction by EUCLID:52; ::_thesis: verum end; supposeA64: ( i3 = i4 & j4 + 1 = j3 ) ; ::_thesis: contradiction (G * (i3,j3)) `1 = (G * (i3,1)) `1 by A59, A60, A56, GOBOARD5:2 .= (E-max (L~ f)) `1 by A4, A6, A12, A17, A21, A54, A64, GOBOARD5:2 .= E-bound (L~ f) by EUCLID:52 ; then G * (i3,j3) in E-most (L~ f) by A14, A49, A57, GOBOARD1:1, SPRECT_2:13; then (G * (i4,j4)) `2 >= (G * (i3,j3)) `2 by A4, A45, A53, A51, PSCOMP_1:47; then j4 >= j4 + 1 by A12, A17, A54, A55, A56, A64, GOBOARD5:4; hence contradiction by NAT_1:13; ::_thesis: verum end; end; end; A65: k9 + 1 = len f ; now__::_thesis:_contradiction percases ( i4 + 1 = i3 or i4 = i3 + 1 ) by A52, A61; suppose i4 + 1 = i3 ; ::_thesis: contradiction then i4 >= i4 + 1 by A17, A21, A54, A55, A59, A58, A61, GOBOARD5:3; hence contradiction by NAT_1:13; ::_thesis: verum end; supposeA66: i4 = i3 + 1 ; ::_thesis: contradiction (len f) - 1 >= 0 by A46, XREAL_1:19; then (len f) -' 1 = (len f) - 1 by XREAL_0:def_2; then A67: (LSeg (f,k)) /\ (LSeg (f,k9)) = {(f . k)} by A45, JORDAN4:42 .= {(f /. k)} by A19, PARTFUN1:def_6 ; ( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A47, A65, TOPREAL1:21; then f /. (k + 1) in {(f /. k)} by A8, A45, A49, A54, A55, A61, A66, A67, XBOOLE_0:def_4; then A68: f /. (k + 1) = f /. k by TARSKI:def_1; i1 <> i2 by A45; hence contradiction by A5, A6, A7, A8, A68, GOBOARD1:5; ::_thesis: verum end; end; end; hence ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) ; ::_thesis: verum end; suppose ( i2 = i1 + 1 & j1 = j2 ) ; ::_thesis: ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) then i1 >= i1 + 1 by A17, A21, A20, A16, GOBOARD5:3; hence ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) by NAT_1:13; ::_thesis: verum end; supposeA69: ( i1 = i2 & j2 = j1 + 1 ) ; ::_thesis: ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) (G * (i2,j2)) `1 = (G * (i2,1)) `1 by A20, A22, A11, GOBOARD5:2 .= E-bound (L~ f) by A12, A17, A21, A10, A69, GOBOARD5:2 ; then G * (i2,j2) in E-most (L~ f) by A8, A14, A15, GOBOARD1:1, SPRECT_2:13; then (G * (i1,j1)) `2 >= (G * (i2,j2)) `2 by A4, A6, PSCOMP_1:47; then j1 >= j1 + 1 by A12, A17, A11, A69, GOBOARD5:4; hence ( [i2,j2] in Indices G & [i2,(j2 + 1)] in Indices G & f /. k = G * (i2,(j2 + 1)) ) by NAT_1:13; ::_thesis: verum end; end; end; hence ( [i2,(j2 + 1)] in Indices G & [i2,j2] in Indices G & f /. k = G * (i2,(j2 + 1)) ) ; ::_thesis: f /. (k + 1) = G * (i2,j2) thus f /. (k + 1) = G * (i2,j2) by A8; ::_thesis: verum end; theorem Th24: :: JORDAN1I:24 for f being non constant standard clockwise_oriented special_circular_sequence for G being Go-board for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) holds ex i, j being Element of NAT st ( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) ) proof let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: for G being Go-board for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) holds ex i, j being Element of NAT st ( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) ) let G be Go-board; ::_thesis: for k being Element of NAT st f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) holds ex i, j being Element of NAT st ( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) ) let k be Element of NAT ; ::_thesis: ( f is_sequence_on G & 1 <= k & k + 1 <= len f & f /. k = S-max (L~ f) implies ex i, j being Element of NAT st ( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) ) ) assume that A1: f is_sequence_on G and A2: 1 <= k and A3: k + 1 <= len f and A4: f /. k = S-max (L~ f) ; ::_thesis: ex i, j being Element of NAT st ( [(i + 1),j] in Indices G & [i,j] in Indices G & f /. k = G * ((i + 1),j) & f /. (k + 1) = G * (i,j) ) consider i1, j1, i2, j2 being Element of NAT such that A5: [i1,j1] in Indices G and A6: f /. k = G * (i1,j1) and A7: [i2,j2] in Indices G and A8: f /. (k + 1) = G * (i2,j2) and A9: ( ( 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, A2, A3, JORDAN8:3; A10: (G * (i1,j1)) `2 = S-bound (L~ f) by A4, A6, EUCLID:52; A11: 1 <= j2 by A7, MATRIX_1:38; take i2 ; ::_thesis: ex j being Element of NAT st ( [(i2 + 1),j] in Indices G & [i2,j] in Indices G & f /. k = G * ((i2 + 1),j) & f /. (k + 1) = G * (i2,j) ) take j2 ; ::_thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) & f /. (k + 1) = G * (i2,j2) ) A12: i1 <= len G by A5, MATRIX_1:38; A13: k + 1 >= 1 + 1 by A2, XREAL_1:7; then A14: len f >= 2 by A3, XXREAL_0:2; k + 1 >= 1 by NAT_1:11; then A15: k + 1 in dom f by A3, FINSEQ_3:25; then f /. (k + 1) in L~ f by A3, A13, GOBOARD1:1, XXREAL_0:2; then A16: (G * (i1,j1)) `2 <= (G * (i2,j2)) `2 by A8, A10, PSCOMP_1:24; A17: 1 <= j1 by A5, MATRIX_1:38; A18: k < len f by A3, NAT_1:13; then A19: k in dom f by A2, FINSEQ_3:25; A20: i2 <= len G by A7, MATRIX_1:38; A21: ( 1 <= i1 & j1 <= width G ) by A5, MATRIX_1:38; A22: ( 1 <= i2 & j2 <= width G ) by A7, MATRIX_1:38; now__::_thesis:_(_[(i2_+_1),j2]_in_Indices_G_&_[i2,j2]_in_Indices_G_&_f_/._k_=_G_*_((i2_+_1),j2)_) percases ( ( i2 + 1 = i1 & j1 = j2 ) or ( i1 = i2 & j1 + 1 = j2 & k <> 1 ) or ( i1 = i2 & j1 + 1 = j2 & k = 1 ) or ( i1 = i2 & j1 = j2 + 1 ) or ( i2 = i1 + 1 & j1 = j2 ) ) by A9; suppose ( i2 + 1 = i1 & j1 = j2 ) ; ::_thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) by A5, A6, A7; ::_thesis: verum end; supposeA23: ( i1 = i2 & j1 + 1 = j2 & k <> 1 ) ; ::_thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) reconsider k9 = k - 1 as Element of NAT by A19, FINSEQ_3:26; k > 1 by A2, A23, XXREAL_0:1; then k >= 1 + 1 by NAT_1:13; then A24: k9 >= (1 + 1) - 1 by XREAL_1:9; then consider i3, j3, i4, j4 being Element of NAT such that A25: [i3,j3] in Indices G and A26: f /. k9 = G * (i3,j3) and A27: [i4,j4] in Indices G and A28: f /. (k9 + 1) = G * (i4,j4) and A29: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A18, JORDAN8:3; A30: i1 = i4 by A5, A6, A27, A28, GOBOARD1:5; k9 + 1 < len f by A3, NAT_1:13; then k9 < len f by NAT_1:13; then A31: k9 in dom f by A24, FINSEQ_3:25; A32: i3 <= len G by A25, MATRIX_1:38; A33: 1 <= j3 by A25, MATRIX_1:38; A34: j1 = j4 by A5, A6, A27, A28, GOBOARD1:5; A35: ( 1 <= i3 & j3 <= width G ) by A25, MATRIX_1:38; A36: i3 = i4 proof assume A37: i3 <> i4 ; ::_thesis: contradiction percases ( ( j3 = j4 & i4 = i3 + 1 ) or ( j3 = j4 & i4 + 1 = i3 ) ) by A29, A37; supposeA38: ( j3 = j4 & i4 = i3 + 1 ) ; ::_thesis: contradiction then (G * (i3,j3)) `2 <> S-bound (L~ f) by A1, A18, A24, A25, A26, A27, A28, Th19; then (G * (1,j3)) `2 <> S-bound (L~ f) by A32, A33, A35, GOBOARD5:1; then (S-max (L~ f)) `2 <> S-bound (L~ f) by A4, A6, A12, A17, A21, A34, A38, GOBOARD5:1; hence contradiction by EUCLID:52; ::_thesis: verum end; supposeA39: ( j3 = j4 & i4 + 1 = i3 ) ; ::_thesis: contradiction (G * (i3,j3)) `2 = (G * (1,j3)) `2 by A32, A33, A35, GOBOARD5:1 .= (S-max (L~ f)) `2 by A4, A6, A12, A17, A21, A34, A39, GOBOARD5:1 .= S-bound (L~ f) by EUCLID:52 ; then G * (i3,j3) in S-most (L~ f) by A14, A26, A31, GOBOARD1:1, SPRECT_2:11; then (G * (i4,j4)) `1 >= (G * (i3,j3)) `1 by A4, A28, PSCOMP_1:55; then i4 >= i4 + 1 by A17, A21, A30, A34, A32, A39, GOBOARD5:3; hence contradiction by NAT_1:13; ::_thesis: verum end; end; end; A40: k9 + 1 = k ; f /. k9 in L~ f by A3, A13, A31, GOBOARD1:1, XXREAL_0:2; then A41: (G * (i1,j1)) `2 <= (G * (i3,j3)) `2 by A10, A26, PSCOMP_1:24; now__::_thesis:_contradiction percases ( j3 + 1 = j4 or j3 = j4 + 1 ) by A29, A36; suppose j3 + 1 = j4 ; ::_thesis: contradiction then j3 >= j3 + 1 by A12, A21, A30, A34, A33, A41, A36, GOBOARD5:4; hence contradiction by NAT_1:13; ::_thesis: verum end; supposeA42: j3 = j4 + 1 ; ::_thesis: contradiction k9 + (1 + 1) <= len f by A3; then A43: (LSeg (f,k9)) /\ (LSeg (f,k)) = {(f /. k)} by A24, A40, TOPREAL1:def_6; ( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A18, A24, A40, TOPREAL1:21; then f /. (k + 1) in {(f /. k)} by A8, A23, A26, A30, A34, A36, A42, A43, XBOOLE_0:def_4; then A44: f /. (k + 1) = f /. k by TARSKI:def_1; j1 <> j2 by A23; hence contradiction by A5, A6, A7, A8, A44, GOBOARD1:5; ::_thesis: verum end; end; end; hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) ; ::_thesis: verum end; supposeA45: ( i1 = i2 & j1 + 1 = j2 & k = 1 ) ; ::_thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) set k1 = len f; k < len f by A3, NAT_1:13; then A46: len f > 1 + 0 by A2, XXREAL_0:2; then len f in dom f by FINSEQ_3:25; then reconsider k9 = (len f) - 1 as Element of NAT by FINSEQ_3:26; k + 1 >= 1 + 1 by A2, XREAL_1:7; then len f >= 1 + 1 by A3, XXREAL_0:2; then A47: k9 >= (1 + 1) - 1 by XREAL_1:9; then consider i3, j3, i4, j4 being Element of NAT such that A48: [i3,j3] in Indices G and A49: f /. k9 = G * (i3,j3) and A50: [i4,j4] in Indices G and A51: f /. (k9 + 1) = G * (i4,j4) and A52: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, JORDAN8:3; A53: f /. (len f) = f /. 1 by FINSEQ_6:def_1; then A54: i1 = i4 by A5, A6, A45, A50, A51, GOBOARD1:5; k9 + 1 <= len f ; then k9 < len f by NAT_1:13; then A55: k9 in dom f by A47, FINSEQ_3:25; then f /. k9 in L~ f by A3, A13, GOBOARD1:1, XXREAL_0:2; then A56: (G * (i1,j1)) `2 <= (G * (i3,j3)) `2 by A10, A49, PSCOMP_1:24; A57: i3 <= len G by A48, MATRIX_1:38; A58: j1 = j4 by A5, A6, A45, A53, A50, A51, GOBOARD1:5; A59: 1 <= j3 by A48, MATRIX_1:38; A60: ( 1 <= i3 & j3 <= width G ) by A48, MATRIX_1:38; A61: i3 = i4 proof assume A62: i3 <> i4 ; ::_thesis: contradiction percases ( ( j3 = j4 & i4 = i3 + 1 ) or ( j3 = j4 & i4 + 1 = i3 ) ) by A52, A62; supposeA63: ( j3 = j4 & i4 = i3 + 1 ) ; ::_thesis: contradiction then (G * (i3,j3)) `2 <> S-bound (L~ f) by A1, A47, A48, A49, A50, A51, Th19; then (G * (1,j3)) `2 <> S-bound (L~ f) by A57, A59, A60, GOBOARD5:1; then (S-max (L~ f)) `2 <> S-bound (L~ f) by A4, A6, A12, A17, A21, A58, A63, GOBOARD5:1; hence contradiction by EUCLID:52; ::_thesis: verum end; supposeA64: ( j3 = j4 & i4 + 1 = i3 ) ; ::_thesis: contradiction (G * (i3,j3)) `2 = (G * (1,j3)) `2 by A57, A59, A60, GOBOARD5:1 .= (S-max (L~ f)) `2 by A4, A6, A12, A17, A21, A58, A64, GOBOARD5:1 .= S-bound (L~ f) by EUCLID:52 ; then G * (i3,j3) in S-most (L~ f) by A14, A49, A55, GOBOARD1:1, SPRECT_2:11; then (G * (i4,j4)) `1 >= (G * (i3,j3)) `1 by A4, A45, A53, A51, PSCOMP_1:55; then i4 >= i4 + 1 by A17, A21, A54, A58, A57, A64, GOBOARD5:3; hence contradiction by NAT_1:13; ::_thesis: verum end; end; end; A65: k9 + 1 = len f ; now__::_thesis:_contradiction percases ( j3 + 1 = j4 or j3 = j4 + 1 ) by A52, A61; suppose j3 + 1 = j4 ; ::_thesis: contradiction then j3 >= j3 + 1 by A12, A21, A54, A58, A59, A56, A61, GOBOARD5:4; hence contradiction by NAT_1:13; ::_thesis: verum end; supposeA66: j3 = j4 + 1 ; ::_thesis: contradiction (len f) - 1 >= 0 by A46, XREAL_1:19; then (len f) -' 1 = (len f) - 1 by XREAL_0:def_2; then A67: (LSeg (f,k)) /\ (LSeg (f,k9)) = {(f . k)} by A45, JORDAN4:42 .= {(f /. k)} by A19, PARTFUN1:def_6 ; ( f /. k9 in LSeg (f,k9) & f /. (k + 1) in LSeg (f,k) ) by A2, A3, A47, A65, TOPREAL1:21; then f /. (k + 1) in {(f /. k)} by A8, A45, A49, A54, A58, A61, A66, A67, XBOOLE_0:def_4; then A68: f /. (k + 1) = f /. k by TARSKI:def_1; j1 <> j2 by A45; hence contradiction by A5, A6, A7, A8, A68, GOBOARD1:5; ::_thesis: verum end; end; end; hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) ; ::_thesis: verum end; suppose ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) then j2 >= j2 + 1 by A12, A21, A11, A16, GOBOARD5:4; hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) by NAT_1:13; ::_thesis: verum end; supposeA69: ( i2 = i1 + 1 & j1 = j2 ) ; ::_thesis: ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) (G * (i2,j2)) `2 = (G * (1,j2)) `2 by A20, A11, A22, GOBOARD5:1 .= S-bound (L~ f) by A12, A17, A21, A10, A69, GOBOARD5:1 ; then G * (i2,j2) in S-most (L~ f) by A8, A14, A15, GOBOARD1:1, SPRECT_2:11; then (G * (i1,j1)) `1 >= (G * (i2,j2)) `1 by A4, A6, PSCOMP_1:55; then i1 >= i1 + 1 by A17, A21, A20, A69, GOBOARD5:3; hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) by NAT_1:13; ::_thesis: verum end; end; end; hence ( [(i2 + 1),j2] in Indices G & [i2,j2] in Indices G & f /. k = G * ((i2 + 1),j2) ) ; ::_thesis: f /. (k + 1) = G * (i2,j2) thus f /. (k + 1) = G * (i2,j2) by A8; ::_thesis: verum end; theorem :: JORDAN1I:25 for f being non constant standard special_circular_sequence holds ( f is clockwise_oriented iff (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) ) proof set i = 1; let f be non constant standard special_circular_sequence; ::_thesis: ( f is clockwise_oriented iff (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) ) set r = Rotate (f,(W-min (L~ f))); A1: Rotate (f,(W-min (L~ f))) is_sequence_on GoB (Rotate (f,(W-min (L~ f)))) by GOBOARD5:def_5; A2: 1 + 1 <= len (Rotate (f,(W-min (L~ f)))) by TOPREAL8:3; then A3: Int (left_cell ((Rotate (f,(W-min (L~ f)))),1)) c= LeftComp (Rotate (f,(W-min (L~ f)))) by GOBOARD9:21; set j = i_s_w (Rotate (f,(W-min (L~ f)))); A4: W-min (L~ f) in rng f by SPRECT_2:43; then A5: (Rotate (f,(W-min (L~ f)))) /. 1 = W-min (L~ f) by FINSEQ_6:92; A6: 2 <= len f by TOPREAL8:3; thus ( f is clockwise_oriented implies (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) ) ::_thesis: ( (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) implies f is clockwise_oriented ) proof set k = (W-min (L~ f)) .. f; (W-min (L~ f)) .. f < len f by SPRECT_5:20; then A7: ((W-min (L~ f)) .. f) + 1 <= len f by NAT_1:13; 1 <= ((W-min (L~ f)) .. f) + 1 by NAT_1:11; then A8: ((W-min (L~ f)) .. f) + 1 in dom f by A7, FINSEQ_3:25; then f /. (((W-min (L~ f)) .. f) + 1) = f . (((W-min (L~ f)) .. f) + 1) by PARTFUN1:def_6; then A9: f /. (((W-min (L~ f)) .. f) + 1) in rng f by A8, FUNCT_1:3; A10: rng f c= L~ f by A6, SPPOL_2:18; A11: f /. ((W-min (L~ f)) .. f) = W-min (L~ f) by A4, FINSEQ_5:38; (W-min (L~ f)) .. f <= ((W-min (L~ f)) .. f) + 1 by NAT_1:13; then A12: f /. (((W-min (L~ f)) .. f) + 1) = (Rotate (f,(W-min (L~ f)))) /. (((((W-min (L~ f)) .. f) + 1) + 1) -' ((W-min (L~ f)) .. f)) by A4, A7, REVROT_1:10 .= (Rotate (f,(W-min (L~ f)))) /. ((((W-min (L~ f)) .. f) + (1 + 1)) -' ((W-min (L~ f)) .. f)) .= (Rotate (f,(W-min (L~ f)))) /. 2 by NAT_D:34 ; f is_sequence_on GoB f by GOBOARD5:def_5; then A13: f is_sequence_on GoB (Rotate (f,(W-min (L~ f)))) by REVROT_1:28; assume f is clockwise_oriented ; ::_thesis: (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) then consider i, j being Element of NAT such that A14: [i,j] in Indices (GoB (Rotate (f,(W-min (L~ f))))) and A15: [i,(j + 1)] in Indices (GoB (Rotate (f,(W-min (L~ f))))) and A16: f /. ((W-min (L~ f)) .. f) = (GoB (Rotate (f,(W-min (L~ f))))) * (i,j) and A17: f /. (((W-min (L~ f)) .. f) + 1) = (GoB (Rotate (f,(W-min (L~ f))))) * (i,(j + 1)) by A4, A7, A11, A13, Th21, FINSEQ_4:21; A18: ( 1 <= i & i <= len (GoB (Rotate (f,(W-min (L~ f))))) ) by A14, MATRIX_1:38; A19: ( 1 <= j + 1 & j + 1 <= width (GoB (Rotate (f,(W-min (L~ f))))) ) by A15, MATRIX_1:38; A20: ( 1 <= j & j <= width (GoB (Rotate (f,(W-min (L~ f))))) ) by A14, MATRIX_1:38; ( 1 <= i & i <= len (GoB (Rotate (f,(W-min (L~ f))))) ) by A14, MATRIX_1:38; then (f /. (((W-min (L~ f)) .. f) + 1)) `1 = ((GoB (Rotate (f,(W-min (L~ f))))) * (i,1)) `1 by A17, A19, GOBOARD5:2 .= (f /. ((W-min (L~ f)) .. f)) `1 by A16, A18, A20, GOBOARD5:2 .= W-bound (L~ f) by A11, EUCLID:52 ; hence (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) by A12, A9, A10, SPRECT_2:12; ::_thesis: verum end; A21: [1,(i_s_w (Rotate (f,(W-min (L~ f)))))] in Indices (GoB (Rotate (f,(W-min (L~ f))))) by JORDAN5D:def_1; then A22: ( 1 <= len (GoB (Rotate (f,(W-min (L~ f))))) & i_s_w (Rotate (f,(W-min (L~ f)))) <= width (GoB (Rotate (f,(W-min (L~ f))))) ) by MATRIX_1:38; len (Rotate (f,(W-min (L~ f)))) > 2 by TOPREAL8:3; then A23: 1 + 1 in dom (Rotate (f,(W-min (L~ f)))) by FINSEQ_3:25; then consider i2, j2 being Element of NAT such that A24: [i2,j2] in Indices (GoB (Rotate (f,(W-min (L~ f))))) and A25: (Rotate (f,(W-min (L~ f)))) /. (1 + 1) = (GoB (Rotate (f,(W-min (L~ f))))) * (i2,j2) by A1, GOBOARD1:def_9; A26: 1 <= j2 by A24, MATRIX_1:38; A27: L~ (Rotate (f,(W-min (L~ f)))) = L~ f by REVROT_1:33; then A28: (GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f)))))) = (Rotate (f,(W-min (L~ f)))) /. 1 by A5, JORDAN5D:def_1; assume A29: (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) ; ::_thesis: f is clockwise_oriented then ((GoB (Rotate (f,(W-min (L~ f))))) * (i2,j2)) `1 = ((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `1 by A5, A28, A25, PSCOMP_1:31; then A30: i2 = 1 by A21, A24, JORDAN1G:7; rng (Rotate (f,(W-min (L~ f)))) = rng f by FINSEQ_6:90, SPRECT_2:43; then 1 in dom (Rotate (f,(W-min (L~ f)))) by FINSEQ_3:31, SPRECT_2:43; then (abs (1 - 1)) + (abs ((i_s_w (Rotate (f,(W-min (L~ f))))) - j2)) = 1 by A1, A21, A28, A23, A24, A25, A30, GOBOARD1:def_9; then 0 + (abs ((i_s_w (Rotate (f,(W-min (L~ f))))) - j2)) = 1 by ABSVALUE:2; then A31: abs (j2 - (i_s_w (Rotate (f,(W-min (L~ f)))))) = 1 by UNIFORM1:11; ((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `2 <= ((GoB (Rotate (f,(W-min (L~ f))))) * (i2,j2)) `2 by A5, A28, A29, A25, PSCOMP_1:31; then j2 - (i_s_w (Rotate (f,(W-min (L~ f))))) >= 0 by A22, A30, A26, GOBOARD5:4, XREAL_1:48; then A32: j2 - (i_s_w (Rotate (f,(W-min (L~ f))))) = 1 by A31, ABSVALUE:def_1; then j2 = (i_s_w (Rotate (f,(W-min (L~ f))))) + 1 ; then ( 1 -' 1 = 1 - 1 & left_cell ((Rotate (f,(W-min (L~ f)))),1,(GoB (Rotate (f,(W-min (L~ f)))))) = cell ((GoB (Rotate (f,(W-min (L~ f))))),(1 -' 1),(i_s_w (Rotate (f,(W-min (L~ f)))))) ) by A2, A1, A21, A28, A24, A25, A30, GOBRD13:21, XREAL_1:233; then A33: left_cell ((Rotate (f,(W-min (L~ f)))),1) = cell ((GoB (Rotate (f,(W-min (L~ f))))),0,(i_s_w (Rotate (f,(W-min (L~ f)))))) by A2, JORDAN1H:21; Int (left_cell ((Rotate (f,(W-min (L~ f)))),1)) <> {} by A2, GOBOARD9:15; then consider p being set such that A34: p in Int (left_cell ((Rotate (f,(W-min (L~ f)))),1)) by XBOOLE_0:def_1; reconsider p = p as Point of (TOP-REAL 2) by A34; A35: ( LeftComp (Rotate (f,(W-min (L~ f)))) is_a_component_of (L~ (Rotate (f,(W-min (L~ f))))) ` & UBD (L~ (Rotate (f,(W-min (L~ f))))) is_a_component_of (L~ (Rotate (f,(W-min (L~ f))))) ` ) by GOBOARD9:def_1, JORDAN2C:124; A36: 1 <= i_s_w (Rotate (f,(W-min (L~ f)))) by A21, MATRIX_1:38; (i_s_w (Rotate (f,(W-min (L~ f))))) + 1 <= width (GoB (Rotate (f,(W-min (L~ f))))) by A24, A32, MATRIX_1:38; then i_s_w (Rotate (f,(W-min (L~ f)))) < width (GoB (Rotate (f,(W-min (L~ f))))) by NAT_1:13; then Int (left_cell ((Rotate (f,(W-min (L~ f)))),1)) = { |[t,s]| where t, s is Real : ( t < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,1)) `1 & ((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `2 < s & s < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,((i_s_w (Rotate (f,(W-min (L~ f))))) + 1))) `2 ) } by A36, A33, GOBOARD6:20; then consider t, s being Real such that A37: p = |[t,s]| and A38: t < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,1)) `1 and ((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `2 < s and s < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,((i_s_w (Rotate (f,(W-min (L~ f))))) + 1))) `2 by A34; now__::_thesis:_not_west_halfline_p_meets_L~_(Rotate_(f,(W-min_(L~_f)))) A39: ((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `1 = ((GoB (Rotate (f,(W-min (L~ f))))) * (1,1)) `1 by A36, A22, GOBOARD5:2; assume west_halfline p meets L~ (Rotate (f,(W-min (L~ f)))) ; ::_thesis: contradiction then (west_halfline p) /\ (L~ (Rotate (f,(W-min (L~ f))))) <> {} by XBOOLE_0:def_7; then consider a being set such that A40: a in (west_halfline p) /\ (L~ (Rotate (f,(W-min (L~ f))))) by XBOOLE_0:def_1; A41: a in L~ (Rotate (f,(W-min (L~ f)))) by A40, XBOOLE_0:def_4; A42: a in west_halfline p by A40, XBOOLE_0:def_4; reconsider a = a as Point of (TOP-REAL 2) by A40; a `1 <= p `1 by A42, TOPREAL1:def_13; then a `1 <= t by A37, EUCLID:52; then a `1 < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `1 by A38, A39, XXREAL_0:2; then a `1 < W-bound (L~ (Rotate (f,(W-min (L~ f))))) by A27, A5, A28, EUCLID:52; hence contradiction by A41, PSCOMP_1:24; ::_thesis: verum end; then A43: west_halfline p c= UBD (L~ (Rotate (f,(W-min (L~ f))))) by JORDAN2C:126; p in west_halfline p by TOPREAL1:38; then LeftComp (Rotate (f,(W-min (L~ f)))) meets UBD (L~ (Rotate (f,(W-min (L~ f))))) by A3, A34, A43, XBOOLE_0:3; then Rotate (f,(W-min (L~ f))) is clockwise_oriented by A35, GOBOARD9:1, JORDAN1H:41; hence f is clockwise_oriented by JORDAN1H:40; ::_thesis: verum end; theorem :: JORDAN1I:26 for f being non constant standard special_circular_sequence holds ( f is clockwise_oriented iff (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) ) proof let f be non constant standard special_circular_sequence; ::_thesis: ( f is clockwise_oriented iff (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) ) set r = Rotate (f,(E-max (L~ f))); set j = i_n_e (Rotate (f,(E-max (L~ f)))); set i = len (GoB (Rotate (f,(E-max (L~ f))))); A1: ( 1 + 1 <= len (Rotate (f,(E-max (L~ f)))) & Rotate (f,(E-max (L~ f))) is_sequence_on GoB (Rotate (f,(E-max (L~ f)))) ) by GOBOARD5:def_5, TOPREAL8:3; A2: E-max (L~ f) in rng f by SPRECT_2:46; then A3: (Rotate (f,(E-max (L~ f)))) /. 1 = E-max (L~ f) by FINSEQ_6:92; A4: 2 <= len f by TOPREAL8:3; thus ( f is clockwise_oriented implies (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) ) ::_thesis: ( (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) implies f is clockwise_oriented ) proof set k = (E-max (L~ f)) .. f; (E-max (L~ f)) .. f < len f by SPRECT_5:16; then A5: ((E-max (L~ f)) .. f) + 1 <= len f by NAT_1:13; 1 <= ((E-max (L~ f)) .. f) + 1 by NAT_1:11; then A6: ((E-max (L~ f)) .. f) + 1 in dom f by A5, FINSEQ_3:25; then f /. (((E-max (L~ f)) .. f) + 1) = f . (((E-max (L~ f)) .. f) + 1) by PARTFUN1:def_6; then A7: f /. (((E-max (L~ f)) .. f) + 1) in rng f by A6, FUNCT_1:3; A8: rng f c= L~ f by A4, SPPOL_2:18; A9: f /. ((E-max (L~ f)) .. f) = E-max (L~ f) by A2, FINSEQ_5:38; (E-max (L~ f)) .. f <= ((E-max (L~ f)) .. f) + 1 by NAT_1:13; then A10: f /. (((E-max (L~ f)) .. f) + 1) = (Rotate (f,(E-max (L~ f)))) /. (((((E-max (L~ f)) .. f) + 1) + 1) -' ((E-max (L~ f)) .. f)) by A2, A5, REVROT_1:10 .= (Rotate (f,(E-max (L~ f)))) /. ((((E-max (L~ f)) .. f) + (1 + 1)) -' ((E-max (L~ f)) .. f)) .= (Rotate (f,(E-max (L~ f)))) /. 2 by NAT_D:34 ; f is_sequence_on GoB f by GOBOARD5:def_5; then A11: f is_sequence_on GoB (Rotate (f,(E-max (L~ f)))) by REVROT_1:28; assume f is clockwise_oriented ; ::_thesis: (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) then consider i, j being Element of NAT such that A12: [i,(j + 1)] in Indices (GoB (Rotate (f,(E-max (L~ f))))) and A13: [i,j] in Indices (GoB (Rotate (f,(E-max (L~ f))))) and A14: f /. ((E-max (L~ f)) .. f) = (GoB (Rotate (f,(E-max (L~ f))))) * (i,(j + 1)) and A15: f /. (((E-max (L~ f)) .. f) + 1) = (GoB (Rotate (f,(E-max (L~ f))))) * (i,j) by A2, A5, A9, A11, Th23, FINSEQ_4:21; A16: ( 1 <= j & j <= width (GoB (Rotate (f,(E-max (L~ f))))) ) by A13, MATRIX_1:38; A17: ( 1 <= j + 1 & j + 1 <= width (GoB (Rotate (f,(E-max (L~ f))))) ) by A12, MATRIX_1:38; A18: ( 1 <= i & i <= len (GoB (Rotate (f,(E-max (L~ f))))) ) by A12, MATRIX_1:38; ( 1 <= i & i <= len (GoB (Rotate (f,(E-max (L~ f))))) ) by A12, MATRIX_1:38; then (f /. (((E-max (L~ f)) .. f) + 1)) `1 = ((GoB (Rotate (f,(E-max (L~ f))))) * (i,1)) `1 by A15, A16, GOBOARD5:2 .= (f /. ((E-max (L~ f)) .. f)) `1 by A14, A18, A17, GOBOARD5:2 .= E-bound (L~ f) by A9, EUCLID:52 ; hence (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) by A10, A7, A8, SPRECT_2:13; ::_thesis: verum end; assume A19: (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) ; ::_thesis: f is clockwise_oriented len (Rotate (f,(E-max (L~ f)))) > 2 by TOPREAL8:3; then A20: ( Rotate (f,(E-max (L~ f))) is_sequence_on GoB (Rotate (f,(E-max (L~ f)))) & 1 + 1 in dom (Rotate (f,(E-max (L~ f)))) ) by FINSEQ_3:25, GOBOARD5:def_5; then consider i2, j2 being Element of NAT such that A21: [i2,j2] in Indices (GoB (Rotate (f,(E-max (L~ f))))) and A22: (Rotate (f,(E-max (L~ f)))) /. (1 + 1) = (GoB (Rotate (f,(E-max (L~ f))))) * (i2,j2) by GOBOARD1:def_9; A23: j2 <= width (GoB (Rotate (f,(E-max (L~ f))))) by A21, MATRIX_1:38; A24: [(len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f)))))] in Indices (GoB (Rotate (f,(E-max (L~ f))))) by JORDAN5D:def_4; then A25: 1 <= i_n_e (Rotate (f,(E-max (L~ f)))) by MATRIX_1:38; then A26: [(len (GoB (Rotate (f,(E-max (L~ f)))))),(((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1) + 1)] in Indices (GoB (Rotate (f,(E-max (L~ f))))) by A24, XREAL_1:235; A27: L~ (Rotate (f,(E-max (L~ f)))) = L~ f by REVROT_1:33; then A28: (GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f)))))) = (Rotate (f,(E-max (L~ f)))) /. 1 by A3, JORDAN5D:def_4; then A29: (Rotate (f,(E-max (L~ f)))) /. 1 = (GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1) + 1)) by A25, XREAL_1:235; (GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f)))))) in E-most (L~ (Rotate (f,(E-max (L~ f))))) by A27, A3, A28, PSCOMP_1:50; then ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f))))))) `1 = (E-min (L~ (Rotate (f,(E-max (L~ f)))))) `1 by PSCOMP_1:47; then A30: ((GoB (Rotate (f,(E-max (L~ f))))) * (i2,j2)) `1 = ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f))))))) `1 by A27, A19, A22, PSCOMP_1:47; then A31: i2 = len (GoB (Rotate (f,(E-max (L~ f))))) by A24, A21, JORDAN1G:7; A32: 1 + 1 <= len (Rotate (f,(E-max (L~ f)))) by TOPREAL8:3; then A33: Int (left_cell ((Rotate (f,(E-max (L~ f)))),1)) c= LeftComp (Rotate (f,(E-max (L~ f)))) by GOBOARD9:21; Int (left_cell ((Rotate (f,(E-max (L~ f)))),1)) <> {} by A32, GOBOARD9:15; then consider p being set such that A34: p in Int (left_cell ((Rotate (f,(E-max (L~ f)))),1)) by XBOOLE_0:def_1; reconsider p = p as Point of (TOP-REAL 2) by A34; A35: ( LeftComp (Rotate (f,(E-max (L~ f)))) is_a_component_of (L~ (Rotate (f,(E-max (L~ f))))) ` & UBD (L~ (Rotate (f,(E-max (L~ f))))) is_a_component_of (L~ (Rotate (f,(E-max (L~ f))))) ` ) by GOBOARD9:def_1, JORDAN2C:124; A36: 1 <= j2 by A21, MATRIX_1:38; A37: i_n_e (Rotate (f,(E-max (L~ f)))) <= width (GoB (Rotate (f,(E-max (L~ f))))) by A24, MATRIX_1:38; rng (Rotate (f,(E-max (L~ f)))) = rng f by FINSEQ_6:90, SPRECT_2:46; then 1 in dom (Rotate (f,(E-max (L~ f)))) by FINSEQ_3:31, SPRECT_2:46; then (abs (i2 - i2)) + (abs ((i_n_e (Rotate (f,(E-max (L~ f))))) - j2)) = 1 by A24, A28, A20, A21, A22, A31, GOBOARD1:def_9; then A38: 0 + (abs ((i_n_e (Rotate (f,(E-max (L~ f))))) - j2)) = 1 by ABSVALUE:2; A39: 1 <= len (GoB (Rotate (f,(E-max (L~ f))))) by A24, MATRIX_1:38; ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f))))))) `2 >= ((GoB (Rotate (f,(E-max (L~ f))))) * (i2,j2)) `2 by A3, A28, A19, A22, PSCOMP_1:47; then (i_n_e (Rotate (f,(E-max (L~ f))))) - j2 >= 0 by A39, A25, A31, A23, GOBOARD5:4, XREAL_1:48; then A40: (i_n_e (Rotate (f,(E-max (L~ f))))) - j2 = 1 by A38, ABSVALUE:def_1; then j2 = (i_n_e (Rotate (f,(E-max (L~ f))))) - 1 ; then A41: j2 = (i_n_e (Rotate (f,(E-max (L~ f))))) -' 1 by A25, XREAL_1:233; then ( [(len (GoB (Rotate (f,(E-max (L~ f)))))),((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1)] in Indices (GoB (Rotate (f,(E-max (L~ f))))) & (Rotate (f,(E-max (L~ f)))) /. (1 + 1) = (GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1)) ) by A24, A21, A22, A30, JORDAN1G:7; then left_cell ((Rotate (f,(E-max (L~ f)))),1,(GoB (Rotate (f,(E-max (L~ f)))))) = cell ((GoB (Rotate (f,(E-max (L~ f))))),(len (GoB (Rotate (f,(E-max (L~ f)))))),((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1)) by A1, A26, A29, GOBRD13:27; then A42: left_cell ((Rotate (f,(E-max (L~ f)))),1) = cell ((GoB (Rotate (f,(E-max (L~ f))))),(len (GoB (Rotate (f,(E-max (L~ f)))))),((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1)) by A32, JORDAN1H:21; (i_n_e (Rotate (f,(E-max (L~ f))))) - 1 < (i_n_e (Rotate (f,(E-max (L~ f))))) - 0 by XREAL_1:15; then (i_n_e (Rotate (f,(E-max (L~ f))))) -' 1 < width (GoB (Rotate (f,(E-max (L~ f))))) by A37, A40, A41, XXREAL_0:2; then Int (left_cell ((Rotate (f,(E-max (L~ f)))),1)) = { |[t,s]| where t, s is Real : ( ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),1)) `1 < t & ((GoB (Rotate (f,(E-max (L~ f))))) * (1,((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1))) `2 < s & s < ((GoB (Rotate (f,(E-max (L~ f))))) * (1,(((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1) + 1))) `2 ) } by A36, A41, A42, GOBOARD6:23; then consider t, s being Real such that A43: p = |[t,s]| and A44: ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),1)) `1 < t and ((GoB (Rotate (f,(E-max (L~ f))))) * (1,((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1))) `2 < s and s < ((GoB (Rotate (f,(E-max (L~ f))))) * (1,(((i_n_e (Rotate (f,(E-max (L~ f))))) -' 1) + 1))) `2 by A34; now__::_thesis:_not_east_halfline_p_meets_L~_(Rotate_(f,(E-max_(L~_f)))) assume east_halfline p meets L~ (Rotate (f,(E-max (L~ f)))) ; ::_thesis: contradiction then (east_halfline p) /\ (L~ (Rotate (f,(E-max (L~ f))))) <> {} by XBOOLE_0:def_7; then consider a being set such that A45: a in (east_halfline p) /\ (L~ (Rotate (f,(E-max (L~ f))))) by XBOOLE_0:def_1; A46: a in L~ (Rotate (f,(E-max (L~ f)))) by A45, XBOOLE_0:def_4; A47: a in east_halfline p by A45, XBOOLE_0:def_4; reconsider a = a as Point of (TOP-REAL 2) by A45; a `1 >= p `1 by A47, TOPREAL1:def_11; then A48: a `1 >= t by A43, EUCLID:52; ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),1)) `1 = ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f))))))) `1 by A39, A25, A37, GOBOARD5:2; then a `1 > ((GoB (Rotate (f,(E-max (L~ f))))) * ((len (GoB (Rotate (f,(E-max (L~ f)))))),(i_n_e (Rotate (f,(E-max (L~ f))))))) `1 by A44, A48, XXREAL_0:2; then a `1 > E-bound (L~ (Rotate (f,(E-max (L~ f))))) by A27, A3, A28, EUCLID:52; hence contradiction by A46, PSCOMP_1:24; ::_thesis: verum end; then A49: east_halfline p c= UBD (L~ (Rotate (f,(E-max (L~ f))))) by JORDAN2C:127; p in east_halfline p by TOPREAL1:38; then LeftComp (Rotate (f,(E-max (L~ f)))) meets UBD (L~ (Rotate (f,(E-max (L~ f))))) by A33, A34, A49, XBOOLE_0:3; then Rotate (f,(E-max (L~ f))) is clockwise_oriented by A35, GOBOARD9:1, JORDAN1H:41; hence f is clockwise_oriented by JORDAN1H:40; ::_thesis: verum end; theorem :: JORDAN1I:27 for f being non constant standard special_circular_sequence holds ( f is clockwise_oriented iff (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) ) proof set j = 1; let f be non constant standard special_circular_sequence; ::_thesis: ( f is clockwise_oriented iff (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) ) set r = Rotate (f,(S-max (L~ f))); A1: Rotate (f,(S-max (L~ f))) is_sequence_on GoB (Rotate (f,(S-max (L~ f)))) by GOBOARD5:def_5; len (Rotate (f,(S-max (L~ f)))) > 2 by TOPREAL8:3; then A2: 1 + 1 in dom (Rotate (f,(S-max (L~ f)))) by FINSEQ_3:25; then consider i2, j2 being Element of NAT such that A3: [i2,j2] in Indices (GoB (Rotate (f,(S-max (L~ f))))) and A4: (Rotate (f,(S-max (L~ f)))) /. (1 + 1) = (GoB (Rotate (f,(S-max (L~ f))))) * (i2,j2) by A1, GOBOARD1:def_9; A5: i2 <= len (GoB (Rotate (f,(S-max (L~ f))))) by A3, MATRIX_1:38; set i = i_e_s (Rotate (f,(S-max (L~ f)))); A6: S-max (L~ f) in rng f by SPRECT_2:42; then A7: (Rotate (f,(S-max (L~ f)))) /. 1 = S-max (L~ f) by FINSEQ_6:92; A8: 2 <= len f by TOPREAL8:3; thus ( f is clockwise_oriented implies (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) ) ::_thesis: ( (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) implies f is clockwise_oriented ) proof set k = (S-max (L~ f)) .. f; (S-max (L~ f)) .. f < len f by SPRECT_5:14; then A9: ((S-max (L~ f)) .. f) + 1 <= len f by NAT_1:13; 1 <= ((S-max (L~ f)) .. f) + 1 by NAT_1:11; then A10: ((S-max (L~ f)) .. f) + 1 in dom f by A9, FINSEQ_3:25; then f /. (((S-max (L~ f)) .. f) + 1) = f . (((S-max (L~ f)) .. f) + 1) by PARTFUN1:def_6; then A11: f /. (((S-max (L~ f)) .. f) + 1) in rng f by A10, FUNCT_1:3; A12: rng f c= L~ f by A8, SPPOL_2:18; A13: f /. ((S-max (L~ f)) .. f) = S-max (L~ f) by A6, FINSEQ_5:38; (S-max (L~ f)) .. f <= ((S-max (L~ f)) .. f) + 1 by NAT_1:13; then A14: f /. (((S-max (L~ f)) .. f) + 1) = (Rotate (f,(S-max (L~ f)))) /. (((((S-max (L~ f)) .. f) + 1) + 1) -' ((S-max (L~ f)) .. f)) by A6, A9, REVROT_1:10 .= (Rotate (f,(S-max (L~ f)))) /. ((((S-max (L~ f)) .. f) + (1 + 1)) -' ((S-max (L~ f)) .. f)) .= (Rotate (f,(S-max (L~ f)))) /. 2 by NAT_D:34 ; f is_sequence_on GoB f by GOBOARD5:def_5; then A15: f is_sequence_on GoB (Rotate (f,(S-max (L~ f)))) by REVROT_1:28; assume f is clockwise_oriented ; ::_thesis: (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) then consider i, j being Element of NAT such that A16: [(i + 1),j] in Indices (GoB (Rotate (f,(S-max (L~ f))))) and A17: [i,j] in Indices (GoB (Rotate (f,(S-max (L~ f))))) and A18: f /. ((S-max (L~ f)) .. f) = (GoB (Rotate (f,(S-max (L~ f))))) * ((i + 1),j) and A19: f /. (((S-max (L~ f)) .. f) + 1) = (GoB (Rotate (f,(S-max (L~ f))))) * (i,j) by A6, A9, A13, A15, Th24, FINSEQ_4:21; A20: ( 1 <= i + 1 & i + 1 <= len (GoB (Rotate (f,(S-max (L~ f))))) ) by A16, MATRIX_1:38; A21: ( 1 <= j & j <= width (GoB (Rotate (f,(S-max (L~ f))))) ) by A16, MATRIX_1:38; A22: ( 1 <= j & j <= width (GoB (Rotate (f,(S-max (L~ f))))) ) by A16, MATRIX_1:38; ( 1 <= i & i <= len (GoB (Rotate (f,(S-max (L~ f))))) ) by A17, MATRIX_1:38; then (f /. (((S-max (L~ f)) .. f) + 1)) `2 = ((GoB (Rotate (f,(S-max (L~ f))))) * (1,j)) `2 by A19, A21, GOBOARD5:1 .= (f /. ((S-max (L~ f)) .. f)) `2 by A18, A20, A22, GOBOARD5:1 .= S-bound (L~ f) by A13, EUCLID:52 ; hence (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) by A14, A11, A12, SPRECT_2:11; ::_thesis: verum end; assume A23: (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) ; ::_thesis: f is clockwise_oriented A24: [(i_e_s (Rotate (f,(S-max (L~ f))))),1] in Indices (GoB (Rotate (f,(S-max (L~ f))))) by JORDAN5D:def_6; then A25: 1 <= i_e_s (Rotate (f,(S-max (L~ f)))) by MATRIX_1:38; A26: L~ (Rotate (f,(S-max (L~ f)))) = L~ f by REVROT_1:33; then A27: (GoB (Rotate (f,(S-max (L~ f))))) * ((i_e_s (Rotate (f,(S-max (L~ f))))),1) = (Rotate (f,(S-max (L~ f)))) /. 1 by A7, JORDAN5D:def_6; then ((GoB (Rotate (f,(S-max (L~ f))))) * ((i_e_s (Rotate (f,(S-max (L~ f))))),1)) `2 = S-bound (L~ f) by A7, EUCLID:52 .= (S-min (L~ f)) `2 by EUCLID:52 ; then ((GoB (Rotate (f,(S-max (L~ f))))) * (i2,j2)) `2 = ((GoB (Rotate (f,(S-max (L~ f))))) * ((i_e_s (Rotate (f,(S-max (L~ f))))),1)) `2 by A23, A4, PSCOMP_1:55; then A28: j2 = 1 by A24, A3, JORDAN1G:6; A29: 1 <= width (GoB (Rotate (f,(S-max (L~ f))))) by A24, MATRIX_1:38; rng (Rotate (f,(S-max (L~ f)))) = rng f by FINSEQ_6:90, SPRECT_2:42; then 1 in dom (Rotate (f,(S-max (L~ f)))) by FINSEQ_3:31, SPRECT_2:42; then (abs (1 - 1)) + (abs ((i_e_s (Rotate (f,(S-max (L~ f))))) - i2)) = 1 by A1, A24, A27, A2, A3, A4, A28, GOBOARD1:def_9; then A30: 0 + (abs ((i_e_s (Rotate (f,(S-max (L~ f))))) - i2)) = 1 by ABSVALUE:2; ((GoB (Rotate (f,(S-max (L~ f))))) * (i2,j2)) `1 <= ((GoB (Rotate (f,(S-max (L~ f))))) * ((i_e_s (Rotate (f,(S-max (L~ f))))),1)) `1 by A7, A27, A23, A4, PSCOMP_1:55; then (i_e_s (Rotate (f,(S-max (L~ f))))) - i2 >= 0 by A25, A29, A28, A5, GOBOARD5:3, XREAL_1:48; then A31: (i_e_s (Rotate (f,(S-max (L~ f))))) - i2 = 1 by A30, ABSVALUE:def_1; then i2 = (i_e_s (Rotate (f,(S-max (L~ f))))) - 1 ; then A32: i2 = (i_e_s (Rotate (f,(S-max (L~ f))))) -' 1 by A25, XREAL_1:233; then A33: 1 <= (i_e_s (Rotate (f,(S-max (L~ f))))) -' 1 by A3, MATRIX_1:38; A34: i_e_s (Rotate (f,(S-max (L~ f)))) <= len (GoB (Rotate (f,(S-max (L~ f))))) by A24, MATRIX_1:38; A35: 1 + 1 <= len (Rotate (f,(S-max (L~ f)))) by TOPREAL8:3; then A36: Int (left_cell ((Rotate (f,(S-max (L~ f)))),1)) c= LeftComp (Rotate (f,(S-max (L~ f)))) by GOBOARD9:21; Int (left_cell ((Rotate (f,(S-max (L~ f)))),1)) <> {} by A35, GOBOARD9:15; then consider p being set such that A37: p in Int (left_cell ((Rotate (f,(S-max (L~ f)))),1)) by XBOOLE_0:def_1; [(((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1) + 1),1] in Indices (GoB (Rotate (f,(S-max (L~ f))))) by A24, A25, XREAL_1:235; then ( 1 -' 1 = 1 - 1 & left_cell ((Rotate (f,(S-max (L~ f)))),1,(GoB (Rotate (f,(S-max (L~ f)))))) = cell ((GoB (Rotate (f,(S-max (L~ f))))),((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1),(1 -' 1)) ) by A35, A1, A27, A3, A4, A28, A31, A32, GOBRD13:25, XREAL_1:233; then A38: left_cell ((Rotate (f,(S-max (L~ f)))),1) = cell ((GoB (Rotate (f,(S-max (L~ f))))),((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1),0) by A35, JORDAN1H:21; (i_e_s (Rotate (f,(S-max (L~ f))))) - 1 < i_e_s (Rotate (f,(S-max (L~ f)))) by XREAL_1:146; then (i_e_s (Rotate (f,(S-max (L~ f))))) -' 1 < len (GoB (Rotate (f,(S-max (L~ f))))) by A34, A31, A32, XXREAL_0:2; then A39: Int (left_cell ((Rotate (f,(S-max (L~ f)))),1)) = { |[t,s]| where t, s is Real : ( ((GoB (Rotate (f,(S-max (L~ f))))) * (((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1),1)) `1 < t & t < ((GoB (Rotate (f,(S-max (L~ f))))) * ((((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1) + 1),1)) `1 & s < ((GoB (Rotate (f,(S-max (L~ f))))) * (1,1)) `2 ) } by A33, A38, GOBOARD6:24; reconsider p = p as Point of (TOP-REAL 2) by A37; A40: ( LeftComp (Rotate (f,(S-max (L~ f)))) is_a_component_of (L~ (Rotate (f,(S-max (L~ f))))) ` & UBD (L~ (Rotate (f,(S-max (L~ f))))) is_a_component_of (L~ (Rotate (f,(S-max (L~ f))))) ` ) by GOBOARD9:def_1, JORDAN2C:124; consider t, s being Real such that A41: p = |[t,s]| and ((GoB (Rotate (f,(S-max (L~ f))))) * (((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1),1)) `1 < t and t < ((GoB (Rotate (f,(S-max (L~ f))))) * ((((i_e_s (Rotate (f,(S-max (L~ f))))) -' 1) + 1),1)) `1 and A42: s < ((GoB (Rotate (f,(S-max (L~ f))))) * (1,1)) `2 by A39, A37; now__::_thesis:_not_south_halfline_p_meets_L~_(Rotate_(f,(S-max_(L~_f)))) assume south_halfline p meets L~ (Rotate (f,(S-max (L~ f)))) ; ::_thesis: contradiction then (south_halfline p) /\ (L~ (Rotate (f,(S-max (L~ f))))) <> {} by XBOOLE_0:def_7; then consider a being set such that A43: a in (south_halfline p) /\ (L~ (Rotate (f,(S-max (L~ f))))) by XBOOLE_0:def_1; A44: a in L~ (Rotate (f,(S-max (L~ f)))) by A43, XBOOLE_0:def_4; A45: a in south_halfline p by A43, XBOOLE_0:def_4; reconsider a = a as Point of (TOP-REAL 2) by A43; a `2 <= p `2 by A45, TOPREAL1:def_12; then a `2 <= s by A41, EUCLID:52; then A46: a `2 < ((GoB (Rotate (f,(S-max (L~ f))))) * (1,1)) `2 by A42, XXREAL_0:2; ((GoB (Rotate (f,(S-max (L~ f))))) * ((i_e_s (Rotate (f,(S-max (L~ f))))),1)) `2 = ((GoB (Rotate (f,(S-max (L~ f))))) * (1,1)) `2 by A25, A34, A29, GOBOARD5:1; then a `2 < S-bound (L~ (Rotate (f,(S-max (L~ f))))) by A26, A7, A27, A46, EUCLID:52; hence contradiction by A44, PSCOMP_1:24; ::_thesis: verum end; then A47: south_halfline p c= UBD (L~ (Rotate (f,(S-max (L~ f))))) by JORDAN2C:128; p in south_halfline p by TOPREAL1:38; then LeftComp (Rotate (f,(S-max (L~ f)))) meets UBD (L~ (Rotate (f,(S-max (L~ f))))) by A36, A37, A47, XBOOLE_0:3; then Rotate (f,(S-max (L~ f))) is clockwise_oriented by A40, GOBOARD9:1, JORDAN1H:41; hence f is clockwise_oriented by JORDAN1H:40; ::_thesis: verum end; theorem :: JORDAN1I:28 for i, k being Element of NAT for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) ) proof let i, k be Element of NAT ; ::_thesis: for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) ) let C be non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) ) let p be Point of (TOP-REAL 2); ::_thesis: ( p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) implies ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) ) ) assume that A1: p `1 = ((W-bound C) + (E-bound C)) / 2 and A2: i > 0 and A3: 1 <= k and A4: k <= width (Gauge (C,i)) and A5: (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) and A6: p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) ; ::_thesis: ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) ) set f = Lower_Seq (C,i); set G = Gauge (C,i); A7: Center (Gauge (C,i)) <= len (Gauge (C,i)) by JORDAN1B:13; 4 <= len (Gauge (C,i)) by JORDAN8:10; then A8: 1 <= len (Gauge (C,i)) by XXREAL_0:2; 4 <= len (Gauge (C,1)) by JORDAN8:10; then 1 <= len (Gauge (C,1)) by XXREAL_0:2; then A9: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1 by A2, A8, JORDAN1A:36; A10: ( 1 <= Center (Gauge (C,1)) & Center (Gauge (C,1)) <= len (Gauge (C,1)) ) by JORDAN1B:11, JORDAN1B:13; A11: 1 <= Center (Gauge (C,i)) by JORDAN1B:11; then A12: ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1 by A3, A4, A7, GOBOARD5:2; 0 + 1 <= i by A2, NAT_1:13; then A13: ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 by A11, A7, A10, JORDAN1A:43; A14: (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) c= (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) or a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) ) assume A15: a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) ; ::_thesis: a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) then reconsider q = a as Point of (TOP-REAL 2) ; A16: a in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A15, XBOOLE_0:def_4; A17: a in L~ (Lower_Seq (C,i)) by A15, XBOOLE_0:def_4; then q in (L~ (Lower_Seq (C,i))) \/ (L~ (Upper_Seq (C,i))) by XBOOLE_0:def_3; then q in L~ (Cage (C,i)) by JORDAN1E:13; then S-bound (L~ (Cage (C,i))) <= q `2 by PSCOMP_1:24; then A18: ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= q `2 by A7, JORDAN1A:72, JORDAN1B:11; ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A3, A4, A11, A7, JORDAN1A:19; then ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A13, XXREAL_0:2; then A19: q `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A16, TOPREAL1:4; q `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1 by A9, A12, A16, GOBOARD7:5; then q in LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A12, A19, A18, GOBOARD7:7; hence a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) by A17, XBOOLE_0:def_4; ::_thesis: verum end; A20: (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by RLTOPSP1:68; ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A3, A4, A11, A7, JORDAN1A:19; then (Gauge (C,i)) * ((Center (Gauge (C,i))),1) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A9, A12, A13, GOBOARD7:7; then LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) by A20, TOPREAL1:6; then (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) c= (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) by XBOOLE_1:27; then (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) = (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) by A14, XBOOLE_0:def_10; then A21: upper_bound (proj2 .: ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))))) = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) by A2, JORDAN1G:56; A22: ( Lower_Seq (C,i) is_sequence_on Gauge (C,i) & Upper_Arc (L~ (Cage (C,i))) c= L~ (Cage (C,i)) ) by JORDAN1F:12, JORDAN6:61; len (Gauge (C,i)) >= 4 by JORDAN8:10; then width (Gauge (C,i)) >= 4 by JORDAN8:def_1; then 1 <= width (Gauge (C,i)) by XXREAL_0:2; then A23: [(Center (Gauge (C,i))),1] in Indices (Gauge (C,i)) by A11, A7, MATRIX_1:36; [(Center (Gauge (C,i))),k] in Indices (Gauge (C,i)) by A3, A4, A11, A7, MATRIX_1:36; then consider n being Element of NAT such that A24: 1 <= n and A25: n <= k and A26: ((Gauge (C,i)) * ((Center (Gauge (C,i))),n)) `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))))) by A3, A4, A5, A11, A7, A23, A22, JORDAN1F:2, JORDAN1G:46; take n ; ::_thesis: ( 1 <= n & n <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) ) thus 1 <= n by A24; ::_thesis: ( n <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) ) thus n <= width (Gauge (C,i)) by A4, A25, XXREAL_0:2; ::_thesis: p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) then p `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),n)) `1 by A1, A2, A24, JORDAN1G:35; hence p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) by A6, A26, A21, TOPREAL3:6; ::_thesis: verum end;