:: JORDAN1H semantic presentation begin registration let D be non empty with_non-empty_element set ; cluster non empty Relation-like non-empty NAT -defined D * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() FinSequence-yielding finite-support for FinSequence of D * ; existence ex b1 being FinSequence of D * st ( not b1 is empty & b1 is non-empty ) proof consider X being non empty set such that A1: X in D by SETFAM_1:def_10; A2: rng <*<*X*>*> = {<*X*>} by FINSEQ_1:39; <*X*> in D * by A1, FUNCT_7:18; then rng <*<*X*>*> c= D * by A2, ZFMISC_1:31; then reconsider F = <*<*X*>*> as FinSequence of D * by FINSEQ_1:def_4; take F ; ::_thesis: ( not F is empty & F is non-empty ) thus not F is empty ; ::_thesis: F is non-empty assume {} in rng F ; :: according to RELAT_1:def_9 ::_thesis: contradiction hence contradiction by A2; ::_thesis: verum end; end; registration let F be non-empty Function-yielding Function; cluster rngs F -> non-empty ; coherence rngs F is non-empty proof now__::_thesis:_for_n_being_set_st_n_in_dom_(rngs_F)_holds_ not_(rngs_F)_._n_is_empty let n be set ; ::_thesis: ( n in dom (rngs F) implies not (rngs F) . n is empty ) assume n in dom (rngs F) ; ::_thesis: not (rngs F) . n is empty then n in dom F by FUNCT_6:60; then ( (rngs F) . n = rng (F . n) & not F . n is empty ) by FUNCT_1:def_9, FUNCT_6:22; hence not (rngs F) . n is empty ; ::_thesis: verum end; hence rngs F is non-empty by FUNCT_1:def_9; ::_thesis: verum end; end; theorem Th1: :: JORDAN1H:1 for p, q being Point of (TOP-REAL 2) st p <> q holds p in Cl ((LSeg (p,q)) \ {p,q}) proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q implies p in Cl ((LSeg (p,q)) \ {p,q}) ) assume A1: p <> q ; ::_thesis: p in Cl ((LSeg (p,q)) \ {p,q}) for G being Subset of (TOP-REAL 2) st G is open & p in G holds (LSeg (p,q)) \ {p,q} meets G proof reconsider x = p, y = q as Point of (Euclid 2) by TOPREAL3:8; let G be Subset of (TOP-REAL 2); ::_thesis: ( G is open & p in G implies (LSeg (p,q)) \ {p,q} meets G ) assume that A2: G is open and A3: p in G ; ::_thesis: (LSeg (p,q)) \ {p,q} meets G A4: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8; then reconsider P = G as Subset of (TopSpaceMetr (Euclid 2)) ; P is open by A2, A4, PRE_TOPC:30; then consider r being real number such that A5: r > 0 and A6: Ball (x,r) c= P by A3, TOPMETR:15; reconsider r = r as Real by XREAL_0:def_1; A7: r / 2 > 0 by A5, XREAL_1:139; set t = min ((r / 2),((dist (x,y)) / 2)); set s = (min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)); set pp = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q); reconsider z = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) as Point of (Euclid 2) by TOPREAL3:8; reconsider x9 = x, y9 = y, z9 = z as Element of REAL 2 ; reconsider a = x9, b = y9 as Element of 2 -tuples_on REAL ; reconsider u = a - b as Element of REAL 2 ; A8: 0 < dist (x,y) by A1, METRIC_1:7; then 0 < (dist (x,y)) / 2 by XREAL_1:139; then A9: 0 < min ((r / 2),((dist (x,y)) / 2)) by A7, XXREAL_0:21; dist (x,z) = |.(x9 - z9).| by SPPOL_1:5 .= |.((a - ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * a)) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b)).| by RVSUM_1:39 .= |.(((1 * a) - ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * a)) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b)).| by RVSUM_1:52 .= |.(((1 * a) + (((- 1) * (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))))) * a)) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b)).| by RVSUM_1:49 .= |.(((1 + (- (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))))) * a) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * b)).| by RVSUM_1:50 .= |.((((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * a) + (((- 1) * ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * b)).| by RVSUM_1:49 .= |.((((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * a) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * ((- 1) * b))).| by RVSUM_1:49 .= |.(((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (a + ((- 1) * b))).| by RVSUM_1:51 .= |.(((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (a + (- b))).| .= |.(((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (a - b)).| .= (abs ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * |.u.| by EUCLID:11 .= ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * |.(a - b).| by A8, A9, ABSVALUE:def_1 .= ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * (dist (x,y)) by SPPOL_1:5 .= min ((r / 2),((dist (x,y)) / 2)) by A8, XCMPLX_1:87 ; then A10: dist (x,z) <= r / 2 by XXREAL_0:17; r / 2 < r / 1 by A5, XREAL_1:76; then dist (x,z) < r by A10, XXREAL_0:2; then A11: z in Ball (x,r) by METRIC_1:11; A12: ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * p) = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) + ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p by EUCLID:33 .= p by EUCLID:29 ; ( min ((r / 2),((dist (x,y)) / 2)) <= (dist (x,y)) / 2 & (dist (x,y)) / 2 < (dist (x,y)) / 1 ) by A8, XREAL_1:76, XXREAL_0:17; then A13: min ((r / 2),((dist (x,y)) / 2)) < dist (x,y) by XXREAL_0:2; then (min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)) < 1 by A9, XREAL_1:189; then A14: ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) in LSeg (p,q) by A8, A9; A15: ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * q) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) = ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) + ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * q by EUCLID:33 .= q by EUCLID:29 ; A16: 1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) <> 0 by A9, A13, XREAL_1:189; A17: now__::_thesis:_not_((1_-_((min_((r_/_2),((dist_(x,y))_/_2)))_/_(dist_(x,y))))_*_p)_+_(((min_((r_/_2),((dist_(x,y))_/_2)))_/_(dist_(x,y)))_*_q)_=_q assume ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) = q ; ::_thesis: contradiction then (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * q = (((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q)) - (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) by A15, EUCLID:48 .= (1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p by EUCLID:48 ; hence contradiction by A1, A16, EUCLID:34; ::_thesis: verum end; A18: 0 < (min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)) by A8, A9, XREAL_1:139; now__::_thesis:_not_((1_-_((min_((r_/_2),((dist_(x,y))_/_2)))_/_(dist_(x,y))))_*_p)_+_(((min_((r_/_2),((dist_(x,y))_/_2)))_/_(dist_(x,y)))_*_q)_=_p assume ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) = p ; ::_thesis: contradiction then ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * p = (((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q)) - ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) by A12, EUCLID:48 .= ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q by EUCLID:48 ; hence contradiction by A1, A18, EUCLID:34; ::_thesis: verum end; then not ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) in {p,q} by A17, TARSKI:def_2; then ((1 - ((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y)))) * p) + (((min ((r / 2),((dist (x,y)) / 2))) / (dist (x,y))) * q) in (LSeg (p,q)) \ {p,q} by A14, XBOOLE_0:def_5; hence (LSeg (p,q)) \ {p,q} meets G by A6, A11, XBOOLE_0:3; ::_thesis: verum end; hence p in Cl ((LSeg (p,q)) \ {p,q}) by TOPS_1:12; ::_thesis: verum end; theorem Th2: :: JORDAN1H:2 for p, q being Point of (TOP-REAL 2) st p <> q holds Cl ((LSeg (p,q)) \ {p,q}) = LSeg (p,q) proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q implies Cl ((LSeg (p,q)) \ {p,q}) = LSeg (p,q) ) assume A1: p <> q ; ::_thesis: Cl ((LSeg (p,q)) \ {p,q}) = LSeg (p,q) Cl ((LSeg (p,q)) \ {p,q}) c= Cl (LSeg (p,q)) by PRE_TOPC:19, XBOOLE_1:36; hence Cl ((LSeg (p,q)) \ {p,q}) c= LSeg (p,q) by PRE_TOPC:22; :: according to XBOOLE_0:def_10 ::_thesis: LSeg (p,q) c= Cl ((LSeg (p,q)) \ {p,q}) let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in LSeg (p,q) or e in Cl ((LSeg (p,q)) \ {p,q}) ) ( p in LSeg (p,q) & q in LSeg (p,q) ) by RLTOPSP1:68; then {p,q} c= LSeg (p,q) by ZFMISC_1:32; then A2: LSeg (p,q) = ((LSeg (p,q)) \ {p,q}) \/ {p,q} by XBOOLE_1:45; assume e in LSeg (p,q) ; ::_thesis: e in Cl ((LSeg (p,q)) \ {p,q}) then A3: ( e in (LSeg (p,q)) \ {p,q} or e in {p,q} ) by A2, XBOOLE_0:def_3; percases ( e in (LSeg (p,q)) \ {p,q} or e = p or e = q ) by A3, TARSKI:def_2; supposeA4: e in (LSeg (p,q)) \ {p,q} ; ::_thesis: e in Cl ((LSeg (p,q)) \ {p,q}) (LSeg (p,q)) \ {p,q} c= Cl ((LSeg (p,q)) \ {p,q}) by PRE_TOPC:18; hence e in Cl ((LSeg (p,q)) \ {p,q}) by A4; ::_thesis: verum end; suppose ( e = p or e = q ) ; ::_thesis: e in Cl ((LSeg (p,q)) \ {p,q}) hence e in Cl ((LSeg (p,q)) \ {p,q}) by A1, Th1; ::_thesis: verum end; end; end; theorem :: JORDAN1H:3 for S being Subset of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st p <> q & (LSeg (p,q)) \ {p,q} c= S holds LSeg (p,q) c= Cl S proof let S be Subset of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st p <> q & (LSeg (p,q)) \ {p,q} c= S holds LSeg (p,q) c= Cl S let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q & (LSeg (p,q)) \ {p,q} c= S implies LSeg (p,q) c= Cl S ) assume A1: p <> q ; ::_thesis: ( not (LSeg (p,q)) \ {p,q} c= S or LSeg (p,q) c= Cl S ) assume (LSeg (p,q)) \ {p,q} c= S ; ::_thesis: LSeg (p,q) c= Cl S then Cl ((LSeg (p,q)) \ {p,q}) c= Cl S by PRE_TOPC:19; hence LSeg (p,q) c= Cl S by A1, Th2; ::_thesis: verum end; begin definition func RealOrd -> Relation of REAL equals :: JORDAN1H:def 1 { [r,s] where r, s is Real : r <= s } ; coherence { [r,s] where r, s is Real : r <= s } is Relation of REAL proof set R = { [r,s] where r, s is Real : r <= s } ; { [r,s] where r, s is Real : r <= s } c= [:REAL,REAL:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [r,s] where r, s is Real : r <= s } or x in [:REAL,REAL:] ) assume x in { [r,s] where r, s is Real : r <= s } ; ::_thesis: x in [:REAL,REAL:] then ex r, s being Real st ( x = [r,s] & r <= s ) ; hence x in [:REAL,REAL:] by ZFMISC_1:87; ::_thesis: verum end; hence { [r,s] where r, s is Real : r <= s } is Relation of REAL ; ::_thesis: verum end; end; :: deftheorem defines RealOrd JORDAN1H:def_1_:_ RealOrd = { [r,s] where r, s is Real : r <= s } ; theorem Th4: :: JORDAN1H:4 for r, s being Real st [r,s] in RealOrd holds r <= s proof let r, s be Real; ::_thesis: ( [r,s] in RealOrd implies r <= s ) hereby ::_thesis: verum assume [r,s] in RealOrd ; ::_thesis: r <= s then consider r1, s1 being Real such that A1: [r,s] = [r1,s1] and A2: r1 <= s1 ; r = r1 by A1, XTUPLE_0:1; hence r <= s by A1, A2, XTUPLE_0:1; ::_thesis: verum end; end; Lm1: RealOrd is_reflexive_in REAL proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in REAL or [x,x] in RealOrd ) assume x in REAL ; ::_thesis: [x,x] in RealOrd then reconsider x = x as Element of REAL ; x <= x ; hence [x,x] in RealOrd ; ::_thesis: verum end; Lm2: RealOrd is_antisymmetric_in REAL proof let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in REAL or not y in REAL or not [x,y] in RealOrd or not [y,x] in RealOrd or x = y ) assume that A1: ( x in REAL & y in REAL ) and A2: ( [x,y] in RealOrd & [y,x] in RealOrd ) ; ::_thesis: x = y reconsider x = x, y = y as Element of REAL by A1; ( x <= y & y <= x ) by A2, Th4; hence x = y by XXREAL_0:1; ::_thesis: verum end; Lm3: RealOrd is_transitive_in REAL proof let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in REAL or not y in REAL or not z in REAL or not [x,y] in RealOrd or not [y,z] in RealOrd or [x,z] in RealOrd ) assume that A1: ( x in REAL & y in REAL & z in REAL ) and A2: ( [x,y] in RealOrd & [y,z] in RealOrd ) ; ::_thesis: [x,z] in RealOrd reconsider x = x, y = y, z = z as Element of REAL by A1; ( x <= y & y <= z ) by A2, Th4; then x <= z by XXREAL_0:2; hence [x,z] in RealOrd ; ::_thesis: verum end; Lm4: RealOrd is_connected_in REAL proof let x, y be set ; :: according to RELAT_2:def_6 ::_thesis: ( not x in REAL or not y in REAL or x = y or [x,y] in RealOrd or [y,x] in RealOrd ) assume ( x in REAL & y in REAL ) ; ::_thesis: ( x = y or [x,y] in RealOrd or [y,x] in RealOrd ) then reconsider x = x, y = y as Element of REAL ; ( x <= y or y <= x ) ; hence ( x = y or [x,y] in RealOrd or [y,x] in RealOrd ) ; ::_thesis: verum end; theorem Th5: :: JORDAN1H:5 field RealOrd = REAL proof field RealOrd c= REAL \/ REAL by RELSET_1:8; hence field RealOrd c= REAL ; :: according to XBOOLE_0:def_10 ::_thesis: REAL c= field RealOrd thus REAL c= field RealOrd by Lm1, PARTIT_2:8; ::_thesis: verum end; registration cluster RealOrd -> total reflexive antisymmetric transitive being_linear-order ; coherence ( RealOrd is total & RealOrd is reflexive & RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order ) proof REAL c= dom RealOrd proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in REAL or x in dom RealOrd ) assume x in REAL ; ::_thesis: x in dom RealOrd then reconsider x = x as Element of REAL ; [x,x] in RealOrd ; hence x in dom RealOrd by XTUPLE_0:def_12; ::_thesis: verum end; then dom RealOrd = REAL by XBOOLE_0:def_10; hence RealOrd is total by PARTFUN1:def_2; ::_thesis: ( RealOrd is reflexive & RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order ) thus RealOrd is reflexive by Lm1, Th5, RELAT_2:def_9; ::_thesis: ( RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order ) thus RealOrd is antisymmetric by Lm2, Th5, RELAT_2:def_12; ::_thesis: ( RealOrd is transitive & RealOrd is being_linear-order ) thus RealOrd is transitive by Lm3, Th5, RELAT_2:def_16; ::_thesis: RealOrd is being_linear-order thus RealOrd is_reflexive_in field RealOrd by Lm1, Th5; :: according to RELAT_2:def_9,ORDERS_1:def_5 ::_thesis: ( RealOrd is transitive & RealOrd is antisymmetric & RealOrd is connected ) thus RealOrd is_transitive_in field RealOrd by Lm3, Th5; :: according to RELAT_2:def_16 ::_thesis: ( RealOrd is antisymmetric & RealOrd is connected ) thus RealOrd is_antisymmetric_in field RealOrd by Lm2, Th5; :: according to RELAT_2:def_12 ::_thesis: RealOrd is connected thus RealOrd is_connected_in field RealOrd by Lm4, Th5; :: according to RELAT_2:def_14 ::_thesis: verum end; end; theorem Th6: :: JORDAN1H:6 RealOrd linearly_orders REAL proof thus RealOrd is_reflexive_in REAL by Lm1; :: according to ORDERS_1:def_8 ::_thesis: ( RealOrd is_transitive_in REAL & RealOrd is_antisymmetric_in REAL & RealOrd is_connected_in REAL ) thus RealOrd is_transitive_in REAL by Lm3; ::_thesis: ( RealOrd is_antisymmetric_in REAL & RealOrd is_connected_in REAL ) thus RealOrd is_antisymmetric_in REAL by Lm2; ::_thesis: RealOrd is_connected_in REAL thus RealOrd is_connected_in REAL by Lm4; ::_thesis: verum end; theorem Th7: :: JORDAN1H:7 for A being finite Subset of REAL holds SgmX (RealOrd,A) is increasing proof let A be finite Subset of REAL; ::_thesis: SgmX (RealOrd,A) is increasing set IT = SgmX (RealOrd,A); let n, m be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: ( not n in dom (SgmX (RealOrd,A)) or not m in dom (SgmX (RealOrd,A)) or m <= n or not (SgmX (RealOrd,A)) . m <= (SgmX (RealOrd,A)) . n ) assume that A1: ( n in dom (SgmX (RealOrd,A)) & m in dom (SgmX (RealOrd,A)) ) and A2: n < m ; ::_thesis: not (SgmX (RealOrd,A)) . m <= (SgmX (RealOrd,A)) . n A3: RealOrd linearly_orders A by Th6, ORDERS_1:38; ( (SgmX (RealOrd,A)) /. n = (SgmX (RealOrd,A)) . n & (SgmX (RealOrd,A)) /. m = (SgmX (RealOrd,A)) . m ) by A1, PARTFUN1:def_6; then [((SgmX (RealOrd,A)) . n),((SgmX (RealOrd,A)) . m)] in RealOrd by A1, A2, A3, PRE_POLY:def_2; then A4: (SgmX (RealOrd,A)) . n <= (SgmX (RealOrd,A)) . m by Th4; SgmX (RealOrd,A) is one-to-one by Th6, ORDERS_1:38, PRE_POLY:10; then (SgmX (RealOrd,A)) . n <> (SgmX (RealOrd,A)) . m by A1, A2, FUNCT_1:def_4; hence not (SgmX (RealOrd,A)) . m <= (SgmX (RealOrd,A)) . n by A4, XXREAL_0:1; ::_thesis: verum end; theorem Th8: :: JORDAN1H:8 for f being FinSequence of REAL for A being finite Subset of REAL st A = rng f holds SgmX (RealOrd,A) = Incr f proof let f be FinSequence of REAL ; ::_thesis: for A being finite Subset of REAL st A = rng f holds SgmX (RealOrd,A) = Incr f let A be finite Subset of REAL; ::_thesis: ( A = rng f implies SgmX (RealOrd,A) = Incr f ) assume A1: A = rng f ; ::_thesis: SgmX (RealOrd,A) = Incr f reconsider F = SgmX (RealOrd,A) as increasing FinSequence of REAL by Th7; RealOrd linearly_orders A by Th6, ORDERS_1:38; then A2: rng (SgmX (RealOrd,A)) = rng f by A1, PRE_POLY:def_2; len F = card (rng f) by A1, Th6, ORDERS_1:38, PRE_POLY:11; hence SgmX (RealOrd,A) = Incr f by A2, SEQ_4:def_21; ::_thesis: verum end; registration let A be finite Subset of REAL; cluster SgmX (RealOrd,A) -> increasing ; coherence SgmX (RealOrd,A) is increasing by Th7; end; theorem Th9: :: JORDAN1H:9 for X being non empty set for A being finite Subset of X for R being being_linear-order Order of X holds len (SgmX (R,A)) = card A proof let X be non empty set ; ::_thesis: for A being finite Subset of X for R being being_linear-order Order of X holds len (SgmX (R,A)) = card A let A be finite Subset of X; ::_thesis: for R being being_linear-order Order of X holds len (SgmX (R,A)) = card A let R be being_linear-order Order of X; ::_thesis: len (SgmX (R,A)) = card A ( field R = X & R linearly_orders field R ) by ORDERS_1:15, ORDERS_1:37; hence len (SgmX (R,A)) = card A by ORDERS_1:38, PRE_POLY:11; ::_thesis: verum end; begin theorem Th10: :: JORDAN1H:10 for f being FinSequence of (TOP-REAL 2) holds X_axis f = proj1 * f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: X_axis f = proj1 * f reconsider pf = proj1 * f as FinSequence of REAL by FINSEQ_2:32; A1: len (X_axis f) = len f by GOBOARD1:def_1; then A2: dom (X_axis f) = dom f by FINSEQ_3:29; A3: for k being Nat st k in dom (X_axis f) holds (X_axis f) . k = pf . k proof let k be Nat; ::_thesis: ( k in dom (X_axis f) implies (X_axis f) . k = pf . k ) assume A4: k in dom (X_axis f) ; ::_thesis: (X_axis f) . k = pf . k A5: f /. k = f . k by A2, A4, PARTFUN1:def_6; thus (X_axis f) . k = (f /. k) `1 by A4, GOBOARD1:def_1 .= proj1 . (f . k) by A5, PSCOMP_1:def_5 .= pf . k by A2, A4, FUNCT_1:13 ; ::_thesis: verum end; len pf = len f by FINSEQ_2:33; then dom (X_axis f) = dom pf by A1, FINSEQ_3:29; hence X_axis f = proj1 * f by A3, FINSEQ_1:13; ::_thesis: verum end; theorem Th11: :: JORDAN1H:11 for f being FinSequence of (TOP-REAL 2) holds Y_axis f = proj2 * f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: Y_axis f = proj2 * f reconsider pf = proj2 * f as FinSequence of REAL by FINSEQ_2:32; A1: len (Y_axis f) = len f by GOBOARD1:def_2; then A2: dom (Y_axis f) = dom f by FINSEQ_3:29; A3: for k being Nat st k in dom (Y_axis f) holds (Y_axis f) . k = pf . k proof let k be Nat; ::_thesis: ( k in dom (Y_axis f) implies (Y_axis f) . k = pf . k ) assume A4: k in dom (Y_axis f) ; ::_thesis: (Y_axis f) . k = pf . k A5: f /. k = f . k by A2, A4, PARTFUN1:def_6; thus (Y_axis f) . k = (f /. k) `2 by A4, GOBOARD1:def_2 .= proj2 . (f . k) by A5, PSCOMP_1:def_6 .= pf . k by A2, A4, FUNCT_1:13 ; ::_thesis: verum end; len pf = len f by FINSEQ_2:33; then dom (Y_axis f) = dom pf by A1, FINSEQ_3:29; hence Y_axis f = proj2 * f by A3, FINSEQ_1:13; ::_thesis: verum end; definition let D be non empty set ; let M be FinSequence of D * ; :: original: Values redefine func Values M -> Subset of D; coherence Values M is Subset of D proof set A = { (rng f) where f is Element of D * : f in rng M } ; for X being set st X in { (rng f) where f is Element of D * : f in rng M } holds X c= D proof let X be set ; ::_thesis: ( X in { (rng f) where f is Element of D * : f in rng M } implies X c= D ) assume X in { (rng f) where f is Element of D * : f in rng M } ; ::_thesis: X c= D then ex f being Element of D * st ( X = rng f & f in rng M ) ; hence X c= D ; ::_thesis: verum end; then union { (rng f) where f is Element of D * : f in rng M } c= D by ZFMISC_1:76; hence Values M is Subset of D by MATRIX_1:41; ::_thesis: verum end; end; registration let D be non empty with_non-empty_elements set ; let M be non empty non-empty FinSequence of D * ; cluster Values M -> non empty ; coherence not Values M is empty proof dom (rngs M) = dom M by FUNCT_6:60; then reconsider X = rng (rngs M) as non empty with_non-empty_elements set by RELAT_1:42; Values M = Union (rngs M) by MATRIX_1:def_16 .= union X by CARD_3:def_4 ; hence not Values M is empty ; ::_thesis: verum end; end; theorem Th12: :: JORDAN1H:12 for D being non empty set for M being Matrix of D for i being Element of NAT st i in Seg (width M) holds rng (Col (M,i)) c= Values M proof let D be non empty set ; ::_thesis: for M being Matrix of D for i being Element of NAT st i in Seg (width M) holds rng (Col (M,i)) c= Values M let M be Matrix of D; ::_thesis: for i being Element of NAT st i in Seg (width M) holds rng (Col (M,i)) c= Values M let k be Element of NAT ; ::_thesis: ( k in Seg (width M) implies rng (Col (M,k)) c= Values M ) assume k in Seg (width M) ; ::_thesis: rng (Col (M,k)) c= Values M then A1: ( 1 <= k & k <= width M ) by FINSEQ_1:1; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (Col (M,k)) or e in Values M ) assume e in rng (Col (M,k)) ; ::_thesis: e in Values M then consider u being set such that A2: u in dom (Col (M,k)) and A3: e = (Col (M,k)) . u by FUNCT_1:def_3; reconsider u = u as Element of NAT by A2; A4: 1 <= u by A2, FINSEQ_3:25; A5: len (Col (M,k)) = len M by MATRIX_1:def_8; then u <= len M by A2, FINSEQ_3:25; then A6: [u,k] in Indices M by A4, A1, MATRIX_1:36; A7: Values M = { (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M } by MATRIX_1:45; dom (Col (M,k)) = dom M by A5, FINSEQ_3:29; then (Col (M,k)) . u = M * (u,k) by A2, MATRIX_1:def_8; hence e in Values M by A7, A3, A6; ::_thesis: verum end; theorem Th13: :: JORDAN1H:13 for D being non empty set for M being Matrix of D for i being Element of NAT st i in dom M holds rng (Line (M,i)) c= Values M proof let D be non empty set ; ::_thesis: for M being Matrix of D for i being Element of NAT st i in dom M holds rng (Line (M,i)) c= Values M let M be Matrix of D; ::_thesis: for i being Element of NAT st i in dom M holds rng (Line (M,i)) c= Values M let k be Element of NAT ; ::_thesis: ( k in dom M implies rng (Line (M,k)) c= Values M ) assume k in dom M ; ::_thesis: rng (Line (M,k)) c= Values M then A1: ( 1 <= k & k <= len M ) by FINSEQ_3:25; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng (Line (M,k)) or e in Values M ) assume e in rng (Line (M,k)) ; ::_thesis: e in Values M then consider u being set such that A2: u in dom (Line (M,k)) and A3: e = (Line (M,k)) . u by FUNCT_1:def_3; reconsider u = u as Element of NAT by A2; A4: 1 <= u by A2, FINSEQ_3:25; A5: len (Line (M,k)) = width M by MATRIX_1:def_7; then u <= width M by A2, FINSEQ_3:25; then A6: [k,u] in Indices M by A1, A4, MATRIX_1:36; A7: Values M = { (M * (i,j)) where i, j is Element of NAT : [i,j] in Indices M } by MATRIX_1:45; dom (Line (M,k)) = Seg (width M) by A5, FINSEQ_1:def_3; then (Line (M,k)) . u = M * (k,u) by A2, MATRIX_1:def_7; hence e in Values M by A7, A3, A6; ::_thesis: verum end; theorem Th14: :: JORDAN1H:14 for G being V15() X_increasing-in-column Matrix of (TOP-REAL 2) holds len G <= card (proj1 .: (Values G)) proof let G be V15() X_increasing-in-column Matrix of (TOP-REAL 2); ::_thesis: len G <= card (proj1 .: (Values G)) 0 <> width G by GOBOARD1:def_3; then 1 <= width G by NAT_1:14; then A1: 1 in Seg (width G) by FINSEQ_1:1; then reconsider L = X_axis (Col (G,1)) as increasing FinSequence of REAL by GOBOARD1:def_7; A2: card (rng L) = len L by FINSEQ_4:62 .= len (Col (G,1)) by GOBOARD1:def_1 .= len G by MATRIX_1:def_8 ; A3: rng L = rng (proj1 * (Col (G,1))) by Th10 .= proj1 .: (rng (Col (G,1))) by RELAT_1:127 ; rng (Col (G,1)) c= Values G by A1, Th12; hence len G <= card (proj1 .: (Values G)) by A3, A2, NAT_1:43, RELAT_1:123; ::_thesis: verum end; theorem Th15: :: JORDAN1H:15 for G being X_equal-in-line Matrix of (TOP-REAL 2) holds card (proj1 .: (Values G)) <= len G proof let G be X_equal-in-line Matrix of (TOP-REAL 2); ::_thesis: card (proj1 .: (Values G)) <= len G deffunc H1( Nat) -> Element of REAL = proj1 . (G * ($1,1)); consider f being FinSequence such that A1: len f = len G and A2: for k being Nat st k in dom f holds f . k = H1(k) from FINSEQ_1:sch_2(); A3: dom f = dom G by A1, FINSEQ_3:29; proj1 .: (Values G) c= rng f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj1 .: (Values G) or y in rng f ) A4: Values G = { (G * (i,j)) where i, j is Element of NAT : [i,j] in Indices G } by MATRIX_1:45; assume y in proj1 .: (Values G) ; ::_thesis: y in rng f then consider x being set such that A5: x in the carrier of (TOP-REAL 2) and A6: x in Values G and A7: y = proj1 . x by FUNCT_2:64; consider i, j being Element of NAT such that A8: x = G * (i,j) and A9: [i,j] in Indices G by A6, A4; reconsider x = x as Point of (TOP-REAL 2) by A5; A10: ( 1 <= j & j <= width G ) by A9, MATRIX_1:38; A11: ( 1 <= i & i <= len G ) by A9, MATRIX_1:38; then A12: i in dom G by FINSEQ_3:25; y = x `1 by A7, PSCOMP_1:def_5 .= (G * (i,1)) `1 by A8, A11, A10, GOBOARD5:2 .= proj1 . (G * (i,1)) by PSCOMP_1:def_5 .= f . i by A2, A3, A12 ; hence y in rng f by A3, A12, FUNCT_1:3; ::_thesis: verum end; then card (proj1 .: (Values G)) c= card (dom G) by A3, CARD_1:12; then card (proj1 .: (Values G)) <= card (dom G) by NAT_1:39; hence card (proj1 .: (Values G)) <= len G by CARD_1:62; ::_thesis: verum end; theorem Th16: :: JORDAN1H:16 for G being V15() X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2) holds len G = card (proj1 .: (Values G)) proof let G be V15() X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2); ::_thesis: len G = card (proj1 .: (Values G)) ( len G <= card (proj1 .: (Values G)) & card (proj1 .: (Values G)) <= len G ) by Th14, Th15; hence len G = card (proj1 .: (Values G)) by XXREAL_0:1; ::_thesis: verum end; theorem Th17: :: JORDAN1H:17 for G being V15() Y_increasing-in-line Matrix of (TOP-REAL 2) holds width G <= card (proj2 .: (Values G)) proof let G be V15() Y_increasing-in-line Matrix of (TOP-REAL 2); ::_thesis: width G <= card (proj2 .: (Values G)) 0 <> len G by GOBOARD1:def_3; then 1 <= len G by NAT_1:14; then A1: 1 in dom G by FINSEQ_3:25; then reconsider L = Y_axis (Line (G,1)) as increasing FinSequence of REAL by GOBOARD1:def_6; A2: card (rng L) = len L by FINSEQ_4:62 .= len (Line (G,1)) by GOBOARD1:def_2 .= width G by MATRIX_1:def_7 ; A3: rng L = rng (proj2 * (Line (G,1))) by Th11 .= proj2 .: (rng (Line (G,1))) by RELAT_1:127 ; rng (Line (G,1)) c= Values G by A1, Th13; hence width G <= card (proj2 .: (Values G)) by A3, A2, NAT_1:43, RELAT_1:123; ::_thesis: verum end; theorem Th18: :: JORDAN1H:18 for G being V15() Y_equal-in-column Matrix of (TOP-REAL 2) holds card (proj2 .: (Values G)) <= width G proof let G be V15() Y_equal-in-column Matrix of (TOP-REAL 2); ::_thesis: card (proj2 .: (Values G)) <= width G deffunc H1( Nat) -> Element of REAL = proj2 . (G * (1,$1)); consider f being FinSequence such that A1: len f = width G and A2: for k being Nat st k in dom f holds f . k = H1(k) from FINSEQ_1:sch_2(); A3: dom f = Seg (width G) by A1, FINSEQ_1:def_3; proj2 .: (Values G) c= rng f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj2 .: (Values G) or y in rng f ) A4: Values G = { (G * (i,j)) where i, j is Element of NAT : [i,j] in Indices G } by MATRIX_1:45; assume y in proj2 .: (Values G) ; ::_thesis: y in rng f then consider x being set such that A5: x in the carrier of (TOP-REAL 2) and A6: x in Values G and A7: y = proj2 . x by FUNCT_2:64; consider i, j being Element of NAT such that A8: x = G * (i,j) and A9: [i,j] in Indices G by A6, A4; reconsider x = x as Point of (TOP-REAL 2) by A5; A10: ( 1 <= i & i <= len G ) by A9, MATRIX_1:38; A11: ( 1 <= j & j <= width G ) by A9, MATRIX_1:38; then A12: j in Seg (width G) by FINSEQ_1:1; y = x `2 by A7, PSCOMP_1:def_6 .= (G * (1,j)) `2 by A8, A11, A10, GOBOARD5:1 .= proj2 . (G * (1,j)) by PSCOMP_1:def_6 .= f . j by A2, A3, A12 ; hence y in rng f by A3, A12, FUNCT_1:3; ::_thesis: verum end; then card (proj2 .: (Values G)) c= card (Seg (width G)) by A3, CARD_1:12; then card (proj2 .: (Values G)) <= card (Seg (width G)) by NAT_1:39; hence card (proj2 .: (Values G)) <= width G by FINSEQ_1:57; ::_thesis: verum end; theorem Th19: :: JORDAN1H:19 for G being V15() Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2) holds width G = card (proj2 .: (Values G)) proof let G be V15() Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2); ::_thesis: width G = card (proj2 .: (Values G)) ( width G <= card (proj2 .: (Values G)) & card (proj2 .: (Values G)) <= width G ) by Th17, Th18; hence width G = card (proj2 .: (Values G)) by XXREAL_0:1; ::_thesis: verum end; begin theorem :: JORDAN1H:20 for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (f,k) c= left_cell (f,k,G) proof let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (f,k) c= left_cell (f,k,G) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G implies for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (f,k) c= left_cell (f,k,G) ) assume A1: f is_sequence_on G ; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (f,k) c= left_cell (f,k,G) let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies LSeg (f,k) c= left_cell (f,k,G) ) assume A2: ( 1 <= k & k + 1 <= len f ) ; ::_thesis: LSeg (f,k) c= left_cell (f,k,G) then A3: k in dom f by SEQ_4:134; then consider i1, j1 being Element of NAT such that A4: [i1,j1] in Indices G and A5: f /. k = G * (i1,j1) by A1, GOBOARD1:def_9; A6: k + 1 in dom f by A2, SEQ_4:134; then consider i2, j2 being Element of NAT such that A7: [i2,j2] in Indices G and A8: f /. (k + 1) = G * (i2,j2) by A1, GOBOARD1:def_9; A9: 1 <= i2 by A7, MATRIX_1:38; A10: 1 <= j1 by A4, MATRIX_1:38; left_cell (f,k,G) = left_cell (f,k,G) ; then A11: ( ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k,G) = cell (G,(i1 -' 1),j1) ) or ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k,G) = cell (G,i1,j1) ) or ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k,G) = cell (G,i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k,G) = cell (G,i1,j2) ) ) by A1, A2, A4, A5, A7, A8, GOBRD13:def_3; A12: 1 <= j2 by A7, MATRIX_1:38; A13: j1 <= width G by A4, MATRIX_1:38; A14: j2 <= width G by A7, MATRIX_1:38; A15: i2 <= len G by A7, MATRIX_1:38; A16: 1 <= i1 by A4, MATRIX_1:38; (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A1, A3, A6, A4, A5, A7, A8, GOBOARD1:def_9; then A17: ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( abs (j1 - j2) = 1 & i1 = i2 ) ) by SEQM_3:42; A18: i1 <= len G by A4, MATRIX_1:38; 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 A17, SEQM_3:41; supposeA19: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: LSeg (f,k) c= left_cell (f,k,G) then A20: j1 < width G by A14, NAT_1:13; A21: (i1 -' 1) + 1 = i1 by A16, XREAL_1:235; then i1 -' 1 < len G by A18, NAT_1:13; then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,(i1 -' 1),j1) by A5, A8, A10, A19, A21, A20, GOBOARD5:18; hence LSeg (f,k) c= left_cell (f,k,G) by A2, A11, A19, TOPREAL1:def_3; ::_thesis: verum end; supposeA22: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: LSeg (f,k) c= left_cell (f,k,G) then i1 < len G by A15, NAT_1:13; then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,i1,j1) by A5, A8, A16, A10, A13, A22, GOBOARD5:22; hence LSeg (f,k) c= left_cell (f,k,G) by A2, A11, A22, TOPREAL1:def_3; ::_thesis: verum end; supposeA23: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: LSeg (f,k) c= left_cell (f,k,G) then A24: i2 < len G by A18, NAT_1:13; A25: (j2 -' 1) + 1 = j2 by A12, XREAL_1:235; then j2 -' 1 < width G by A14, NAT_1:13; then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,i2,(j2 -' 1)) by A5, A8, A9, A23, A25, A24, GOBOARD5:21; hence LSeg (f,k) c= left_cell (f,k,G) by A2, A11, A23, TOPREAL1:def_3; ::_thesis: verum end; supposeA26: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: LSeg (f,k) c= left_cell (f,k,G) then j2 < width G by A13, NAT_1:13; then LSeg ((f /. k),(f /. (k + 1))) c= left_cell (f,k,G) by A5, A8, A16, A18, A12, A11, A26, GOBOARD5:19; hence LSeg (f,k) c= left_cell (f,k,G) by A2, TOPREAL1:def_3; ::_thesis: verum end; end; end; theorem :: JORDAN1H:21 for k being Element of NAT for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds left_cell (f,k,(GoB f)) = left_cell (f,k) proof let k be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds left_cell (f,k,(GoB f)) = left_cell (f,k) let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f implies left_cell (f,k,(GoB f)) = left_cell (f,k) ) assume that A1: 1 <= k and A2: k + 1 <= len f ; ::_thesis: left_cell (f,k,(GoB f)) = left_cell (f,k) set G = GoB f; A3: f is_sequence_on GoB f by GOBOARD5:def_5; for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) ) holds ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k) = cell ((GoB f),i1,j2) ) proof 1 <= k + 1 by NAT_1:11; then A4: k + 1 in dom f by A2, FINSEQ_3:25; let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) ) & not ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i1,j1) ) & not ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) ) implies ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k) = cell ((GoB f),i1,j2) ) ) assume A5: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) ) ; ::_thesis: ( ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) ) or ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i1,j1) ) or ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k) = cell ((GoB f),i1,j2) ) ) k < len f by A2, NAT_1:13; then k in dom f by A1, FINSEQ_3:25; then (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A5, A4, GOBOARD1:def_9; then A6: ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( abs (j1 - j2) = 1 & i1 = i2 ) ) by SEQM_3:42; left_cell (f,k) = left_cell (f,k) ; then A7: ( ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) ) or ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i1,j1) ) or ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k) = cell ((GoB f),i1,j2) ) ) by A1, A2, A5, 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 A6, SEQM_3:41; case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) hence left_cell (f,k) = cell ((GoB f),(i1 -' 1),j1) by A7; ::_thesis: verum end; case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: left_cell (f,k) = cell ((GoB f),i1,j1) hence left_cell (f,k) = cell ((GoB f),i1,j1) by A7; ::_thesis: verum end; case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) hence left_cell (f,k) = cell ((GoB f),i2,(j2 -' 1)) by A7; ::_thesis: verum end; case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: left_cell (f,k) = cell ((GoB f),i1,j2) hence left_cell (f,k) = cell ((GoB f),i1,j2) by A7; ::_thesis: verum end; end; end; hence left_cell (f,k,(GoB f)) = left_cell (f,k) by A1, A2, A3, GOBRD13:def_3; ::_thesis: verum end; theorem Th22: :: JORDAN1H:22 for G being Go-board for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (f,k) c= right_cell (f,k,G) proof let G be Go-board; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (f,k) c= right_cell (f,k,G) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on G implies for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (f,k) c= right_cell (f,k,G) ) assume A1: f is_sequence_on G ; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds LSeg (f,k) c= right_cell (f,k,G) let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies LSeg (f,k) c= right_cell (f,k,G) ) assume A2: ( 1 <= k & k + 1 <= len f ) ; ::_thesis: LSeg (f,k) c= right_cell (f,k,G) then A3: k in dom f by SEQ_4:134; then consider i1, j1 being Element of NAT such that A4: [i1,j1] in Indices G and A5: f /. k = G * (i1,j1) by A1, GOBOARD1:def_9; A6: k + 1 in dom f by A2, SEQ_4:134; then consider i2, j2 being Element of NAT such that A7: [i2,j2] in Indices G and A8: f /. (k + 1) = G * (i2,j2) by A1, GOBOARD1:def_9; A9: 1 <= i2 by A7, MATRIX_1:38; A10: 1 <= j1 by A4, MATRIX_1:38; right_cell (f,k,G) = right_cell (f,k,G) ; then A11: ( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k,G) = cell (G,i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k,G) = cell (G,i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k,G) = cell (G,i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k,G) = cell (G,(i1 -' 1),j2) ) ) by A1, A2, A4, A5, A7, A8, GOBRD13:def_2; A12: 1 <= j2 by A7, MATRIX_1:38; A13: j1 <= width G by A4, MATRIX_1:38; A14: j2 <= width G by A7, MATRIX_1:38; A15: i2 <= len G by A7, MATRIX_1:38; A16: 1 <= i1 by A4, MATRIX_1:38; (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A1, A3, A6, A4, A5, A7, A8, GOBOARD1:def_9; then A17: ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( abs (j1 - j2) = 1 & i1 = i2 ) ) by SEQM_3:42; A18: i1 <= len G by A4, MATRIX_1:38; 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 A17, SEQM_3:41; supposeA19: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: LSeg (f,k) c= right_cell (f,k,G) then j1 < width G by A14, NAT_1:13; then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,i1,j1) by A5, A8, A16, A18, A10, A19, GOBOARD5:19; hence LSeg (f,k) c= right_cell (f,k,G) by A2, A11, A19, TOPREAL1:def_3; ::_thesis: verum end; supposeA20: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: LSeg (f,k) c= right_cell (f,k,G) then A21: i1 < len G by A15, NAT_1:13; A22: (j1 -' 1) + 1 = j1 by A10, XREAL_1:235; then j1 -' 1 < width G by A13, NAT_1:13; then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,i1,(j1 -' 1)) by A5, A8, A16, A20, A22, A21, GOBOARD5:21; hence LSeg (f,k) c= right_cell (f,k,G) by A2, A11, A20, TOPREAL1:def_3; ::_thesis: verum end; supposeA23: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: LSeg (f,k) c= right_cell (f,k,G) then i2 < len G by A18, NAT_1:13; then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,i2,j2) by A5, A8, A9, A12, A14, A23, GOBOARD5:22; hence LSeg (f,k) c= right_cell (f,k,G) by A2, A11, A23, TOPREAL1:def_3; ::_thesis: verum end; supposeA24: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: LSeg (f,k) c= right_cell (f,k,G) then A25: j2 < width G by A13, NAT_1:13; A26: (i1 -' 1) + 1 = i1 by A16, XREAL_1:235; then i1 -' 1 < len G by A18, NAT_1:13; then LSeg ((f /. k),(f /. (k + 1))) c= right_cell (f,k,G) by A5, A8, A12, A11, A24, A26, A25, GOBOARD5:18; hence LSeg (f,k) c= right_cell (f,k,G) by A2, TOPREAL1:def_3; ::_thesis: verum end; end; end; theorem Th23: :: JORDAN1H:23 for k being Element of NAT for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds right_cell (f,k,(GoB f)) = right_cell (f,k) proof let k be Element of NAT ; ::_thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds right_cell (f,k,(GoB f)) = right_cell (f,k) let f be standard special_circular_sequence; ::_thesis: ( 1 <= k & k + 1 <= len f implies right_cell (f,k,(GoB f)) = right_cell (f,k) ) assume that A1: 1 <= k and A2: k + 1 <= len f ; ::_thesis: right_cell (f,k,(GoB f)) = right_cell (f,k) set G = GoB f; A3: f is_sequence_on GoB f by GOBOARD5:def_5; for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) ) proof 1 <= k + 1 by NAT_1:11; then A4: k + 1 in dom f by A2, FINSEQ_3:25; set IT = right_cell (f,k); let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k) = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i2,j2) ) implies ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) ) ) assume A5: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) ) ; ::_thesis: ( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k) = cell ((GoB f),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) ) ) k < len f by A2, NAT_1:13; then k in dom f by A1, FINSEQ_3:25; then (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A5, A4, GOBOARD1:def_9; then A6: ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( abs (j1 - j2) = 1 & i1 = i2 ) ) by SEQM_3:42; right_cell (f,k) = right_cell (f,k) ; then A7: ( ( i1 = i2 & j1 + 1 = j2 & right_cell (f,k) = cell ((GoB f),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell (f,k) = cell ((GoB f),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) ) ) by A1, A2, A5, 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 A6, SEQM_3:41; case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: right_cell (f,k) = cell ((GoB f),i1,j1) hence right_cell (f,k) = cell ((GoB f),i1,j1) by A7; ::_thesis: verum end; case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) hence right_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A7; ::_thesis: verum end; case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: right_cell (f,k) = cell ((GoB f),i2,j2) hence right_cell (f,k) = cell ((GoB f),i2,j2) by A7; ::_thesis: verum end; case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) hence right_cell (f,k) = cell ((GoB f),(i1 -' 1),j2) by A7; ::_thesis: verum end; end; end; hence right_cell (f,k,(GoB f)) = right_cell (f,k) by A1, A2, A3, GOBRD13:def_2; ::_thesis: verum end; theorem :: JORDAN1H:24 for P being Subset of (TOP-REAL 2) for f being non constant standard special_circular_sequence holds ( not P is_a_component_of (L~ f) ` or P = RightComp f or P = LeftComp f ) proof let P be Subset of (TOP-REAL 2); ::_thesis: for f being non constant standard special_circular_sequence holds ( not P is_a_component_of (L~ f) ` or P = RightComp f or P = LeftComp f ) let f be non constant standard special_circular_sequence; ::_thesis: ( not P is_a_component_of (L~ f) ` or P = RightComp f or P = LeftComp f ) assume P is_a_component_of (L~ f) ` ; ::_thesis: ( P = RightComp f or P = LeftComp f ) then ex B1 being Subset of ((TOP-REAL 2) | ((L~ f) `)) st ( B1 = P & B1 is a_component ) by CONNSP_1:def_6; hence ( P = RightComp f or P = LeftComp f ) by GOBRD14:12; ::_thesis: verum end; theorem :: JORDAN1H:25 for G being Go-board for f being non constant standard special_circular_sequence st f is_sequence_on G holds for k being Element of NAT st 1 <= k & k + 1 <= len f holds ( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f ) proof let G be Go-board; ::_thesis: for f being non constant standard special_circular_sequence st f is_sequence_on G holds for k being Element of NAT st 1 <= k & k + 1 <= len f holds ( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f ) let f be non constant standard special_circular_sequence; ::_thesis: ( f is_sequence_on G implies for k being Element of NAT st 1 <= k & k + 1 <= len f holds ( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f ) ) assume A1: f is_sequence_on G ; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds ( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f ) let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies ( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f ) ) assume A2: ( 1 <= k & k + 1 <= len f ) ; ::_thesis: ( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f ) Int (right_cell (f,k,G)) misses L~ f by A1, A2, JORDAN9:15; then A3: Int (right_cell (f,k,G)) c= (right_cell (f,k,G)) \ (L~ f) by TOPS_1:16, XBOOLE_1:86; Int (left_cell (f,k,G)) misses L~ f by A1, A2, JORDAN9:15; then A4: Int (left_cell (f,k,G)) c= (left_cell (f,k,G)) \ (L~ f) by TOPS_1:16, XBOOLE_1:86; (right_cell (f,k,G)) \ (L~ f) c= RightComp f by A1, A2, JORDAN9:27; hence Int (right_cell (f,k,G)) c= RightComp f by A3, XBOOLE_1:1; ::_thesis: Int (left_cell (f,k,G)) c= LeftComp f (left_cell (f,k,G)) \ (L~ f) c= LeftComp f by A1, A2, JORDAN9:27; hence Int (left_cell (f,k,G)) c= LeftComp f by A4, XBOOLE_1:1; ::_thesis: verum end; theorem Th26: :: JORDAN1H:26 for i1, j1, i2, j2 being Element of NAT for G being Go-board st [i1,j1] in Indices G & [i2,j2] in Indices G & G * (i1,j1) = G * (i2,j2) holds ( i1 = i2 & j1 = j2 ) proof let i1, j1, i2, j2 be Element of NAT ; ::_thesis: for G being Go-board st [i1,j1] in Indices G & [i2,j2] in Indices G & G * (i1,j1) = G * (i2,j2) holds ( i1 = i2 & j1 = j2 ) let G be Go-board; ::_thesis: ( [i1,j1] in Indices G & [i2,j2] in Indices G & G * (i1,j1) = G * (i2,j2) implies ( i1 = i2 & j1 = j2 ) ) assume that A1: [i1,j1] in Indices G and A2: [i2,j2] in Indices G and A3: G * (i1,j1) = G * (i2,j2) ; ::_thesis: ( i1 = i2 & j1 = j2 ) A4: 1 <= i1 by A1, MATRIX_1:38; A5: j1 <= width G by A1, MATRIX_1:38; A6: 1 <= j1 by A1, MATRIX_1:38; A7: 1 <= i2 by A2, MATRIX_1:38; A8: i1 <= len G by A1, MATRIX_1:38; A9: i2 <= len G by A2, MATRIX_1:38; A10: j2 <= width G by A2, MATRIX_1:38; A11: 1 <= j2 by A2, MATRIX_1:38; then A12: (G * (i1,j2)) `2 = (G * (1,j2)) `2 by A4, A8, A10, GOBOARD5:1 .= (G * (i1,j1)) `2 by A3, A7, A9, A11, A10, GOBOARD5:1 ; A13: (G * (i1,j2)) `1 = (G * (i1,1)) `1 by A4, A8, A11, A10, GOBOARD5:2 .= (G * (i1,j1)) `1 by A4, A8, A6, A5, GOBOARD5:2 ; assume A14: ( not i1 = i2 or not j1 = j2 ) ; ::_thesis: contradiction percases ( i1 < i2 or i1 > i2 or j1 < j2 or j1 > j2 ) by A14, XXREAL_0:1; suppose i1 < i2 ; ::_thesis: contradiction hence contradiction by A3, A4, A9, A11, A10, A13, GOBOARD5:3; ::_thesis: verum end; suppose i1 > i2 ; ::_thesis: contradiction hence contradiction by A3, A8, A7, A11, A10, A13, GOBOARD5:3; ::_thesis: verum end; suppose j1 < j2 ; ::_thesis: contradiction hence contradiction by A4, A8, A6, A10, A12, GOBOARD5:4; ::_thesis: verum end; suppose j1 > j2 ; ::_thesis: contradiction hence contradiction by A4, A8, A5, A11, A12, GOBOARD5:4; ::_thesis: verum end; end; end; theorem Th27: :: JORDAN1H:27 for i1, i2 being Element of NAT for f being FinSequence of (TOP-REAL 2) for M being Go-board st f is_sequence_on M holds mid (f,i1,i2) is_sequence_on M proof let i1, i2 be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) for M being Go-board st f is_sequence_on M holds mid (f,i1,i2) is_sequence_on M let f be FinSequence of (TOP-REAL 2); ::_thesis: for M being Go-board st f is_sequence_on M holds mid (f,i1,i2) is_sequence_on M let M be Go-board; ::_thesis: ( f is_sequence_on M implies mid (f,i1,i2) is_sequence_on M ) assume A1: f is_sequence_on M ; ::_thesis: mid (f,i1,i2) is_sequence_on M percases ( i1 <= i2 or i1 > i2 ) ; supposeA2: i1 <= i2 ; ::_thesis: mid (f,i1,i2) is_sequence_on M A3: f /^ (i1 -' 1) is_sequence_on M by A1, JORDAN8:2; mid (f,i1,i2) = (f /^ (i1 -' 1)) | ((i2 -' i1) + 1) by A2, FINSEQ_6:def_3; hence mid (f,i1,i2) is_sequence_on M by A3, GOBOARD1:22; ::_thesis: verum end; supposeA4: i1 > i2 ; ::_thesis: mid (f,i1,i2) is_sequence_on M f /^ (i2 -' 1) is_sequence_on M by A1, JORDAN8:2; then A5: (f /^ (i2 -' 1)) | ((i1 -' i2) + 1) is_sequence_on M by GOBOARD1:22; mid (f,i1,i2) = Rev ((f /^ (i2 -' 1)) | ((i1 -' i2) + 1)) by A4, FINSEQ_6:def_3; hence mid (f,i1,i2) is_sequence_on M by A5, JORDAN9:5; ::_thesis: verum end; end; end; registration cluster non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column -> non empty non-empty for FinSequence of the carrier of (TOP-REAL 2) * ; coherence for b1 being Go-board holds ( not b1 is empty & b1 is non-empty ) proof let G be Go-board; ::_thesis: ( not G is empty & G is non-empty ) thus not G is empty ; ::_thesis: G is non-empty consider n0 being Nat such that A1: for x being set st x in rng G holds ex s being FinSequence st ( s = x & len s = n0 ) by MATRIX_1:def_1; len G <> 0 by GOBOARD1:def_3; then consider s0 being FinSequence such that A2: s0 in rng G and A3: len s0 = width G by MATRIX_1:def_3; A4: ex s being FinSequence st ( s = s0 & len s = n0 ) by A2, A1; assume not G is non-empty ; ::_thesis: contradiction then consider n being set such that A5: n in dom G and A6: G . n is empty by FUNCT_1:def_9; A7: card (G . n) is empty by A6; ex s1 being FinSequence st ( s1 = G . n & len s1 = n0 ) by A5, A1, FUNCT_1:3; hence contradiction by A3, A4, A7, GOBOARD1:def_3; ::_thesis: verum end; end; theorem Th28: :: JORDAN1H:28 for i being Element of NAT for G being Go-board st 1 <= i & i <= len G holds (SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1 proof let i be Element of NAT ; ::_thesis: for G being Go-board st 1 <= i & i <= len G holds (SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1 let G be Go-board; ::_thesis: ( 1 <= i & i <= len G implies (SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1 ) assume ( 1 <= i & i <= len G ) ; ::_thesis: (SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1 then i in dom G by FINSEQ_3:25; then A1: i in Seg (len G) by FINSEQ_1:def_3; 0 <> width G by GOBOARD1:def_3; then A2: 1 <= width G by NAT_1:14; reconsider A = proj1 .: (Values G) as finite Subset of REAL ; deffunc H1( Nat) -> Element of REAL = (G * ($1,1)) `1 ; consider f being FinSequence of REAL such that A3: len f = len G and A4: for i being Nat st i in dom f holds f . i = H1(i) from FINSEQ_2:sch_1(); A5: dom f = Seg (len G) by A3, FINSEQ_1:def_3; A6: rng f = A proof A7: Values G = { (G * (m,n)) where m, n is Element of NAT : [m,n] in Indices G } by MATRIX_1:45; thus rng f c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in A ) assume A8: x in rng f ; ::_thesis: x in A then reconsider x = x as Element of REAL ; consider y being set such that A9: y in dom f and A10: x = f . y by A8, FUNCT_1:def_3; reconsider y = y as Element of NAT by A9; ( 1 <= y & y <= len G ) by A3, A9, FINSEQ_3:25; then [y,1] in Indices G by A2, MATRIX_1:36; then A11: G * (y,1) in Values G by A7; x = (G * (y,1)) `1 by A4, A9, A10 .= proj1 . (G * (y,1)) by PSCOMP_1:def_5 ; hence x in A by A11, FUNCT_2:35; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in rng f ) assume A12: x in A ; ::_thesis: x in rng f then reconsider x = x as Element of REAL ; consider p being Element of (TOP-REAL 2) such that A13: p in Values G and A14: x = proj1 . p by A12, FUNCT_2:65; consider m, n being Element of NAT such that A15: p = G * (m,n) and A16: [m,n] in Indices G by A7, A13; A17: ( 1 <= n & n <= width G ) by A16, MATRIX_1:38; A18: ( 1 <= m & m <= len G ) by A16, MATRIX_1:38; then A19: m in Seg (len G) by FINSEQ_1:1; A20: m in dom f by A3, A18, FINSEQ_3:25; x = p `1 by A14, PSCOMP_1:def_5 .= (G * (m,1)) `1 by A15, A17, A18, GOBOARD5:2 .= f . m by A4, A5, A19 ; hence x in rng f by A20, FUNCT_1:def_3; ::_thesis: verum end; for n, m being Nat st n in dom f & m in dom f & n < m holds ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd ) proof let n, m be Nat; ::_thesis: ( n in dom f & m in dom f & n < m implies ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd ) ) assume that A21: ( n in dom f & m in dom f ) and A22: n < m ; ::_thesis: ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd ) A23: ( 1 <= n & m <= len G ) by A3, A21, FINSEQ_3:25; reconsider n9 = n, m9 = m as Element of NAT by ORDINAL1:def_12; A24: ( f /. n = f . n & f /. m = f . m ) by A21, PARTFUN1:def_6; A25: ( f . n = (G * (n9,1)) `1 & f . m = (G * (m9,1)) `1 ) by A4, A21; hence f /. n <> f /. m by A2, A22, A23, A24, GOBOARD5:3; ::_thesis: [(f /. n),(f /. m)] in RealOrd f . n9 < f . m9 by A2, A22, A25, A23, GOBOARD5:3; hence [(f /. n),(f /. m)] in RealOrd by A24; ::_thesis: verum end; then f = SgmX (RealOrd,(proj1 .: (Values G))) by A6, PRE_POLY:9; hence (SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1 by A4, A5, A1; ::_thesis: verum end; theorem Th29: :: JORDAN1H:29 for j being Element of NAT for G being Go-board st 1 <= j & j <= width G holds (SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2 proof let j be Element of NAT ; ::_thesis: for G being Go-board st 1 <= j & j <= width G holds (SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2 let G be Go-board; ::_thesis: ( 1 <= j & j <= width G implies (SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2 ) assume ( 1 <= j & j <= width G ) ; ::_thesis: (SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2 then A1: j in Seg (width G) by FINSEQ_1:1; A2: 1 <= len G by NAT_1:14; reconsider A = proj2 .: (Values G) as finite Subset of REAL ; deffunc H1( Nat) -> Element of REAL = (G * (1,$1)) `2 ; consider f being FinSequence of REAL such that A3: len f = width G and A4: for i being Nat st i in dom f holds f . i = H1(i) from FINSEQ_2:sch_1(); A5: dom f = Seg (width G) by A3, FINSEQ_1:def_3; A6: rng f = A proof A7: Values G = { (G * (m,n)) where m, n is Element of NAT : [m,n] in Indices G } by MATRIX_1:45; thus rng f c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in A ) assume A8: x in rng f ; ::_thesis: x in A then reconsider x = x as Element of REAL ; consider y being set such that A9: y in dom f and A10: x = f . y by A8, FUNCT_1:def_3; reconsider y = y as Element of NAT by A9; ( 1 <= y & y <= width G ) by A3, A9, FINSEQ_3:25; then [1,y] in Indices G by A2, MATRIX_1:36; then A11: G * (1,y) in Values G by A7; x = (G * (1,y)) `2 by A4, A9, A10 .= proj2 . (G * (1,y)) by PSCOMP_1:def_6 ; hence x in A by A11, FUNCT_2:35; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in rng f ) assume A12: x in A ; ::_thesis: x in rng f then reconsider x = x as Element of REAL ; consider p being Element of (TOP-REAL 2) such that A13: p in Values G and A14: x = proj2 . p by A12, FUNCT_2:65; consider m, n being Element of NAT such that A15: p = G * (m,n) and A16: [m,n] in Indices G by A7, A13; A17: ( 1 <= m & m <= len G ) by A16, MATRIX_1:38; A18: ( 1 <= n & n <= width G ) by A16, MATRIX_1:38; then A19: n in Seg (width G) by FINSEQ_1:1; A20: n in dom f by A3, A18, FINSEQ_3:25; x = p `2 by A14, PSCOMP_1:def_6 .= (G * (1,n)) `2 by A15, A17, A18, GOBOARD5:1 .= f . n by A4, A5, A19 ; hence x in rng f by A20, FUNCT_1:def_3; ::_thesis: verum end; for n, m being Nat st n in dom f & m in dom f & n < m holds ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd ) proof let n, m be Nat; ::_thesis: ( n in dom f & m in dom f & n < m implies ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd ) ) assume that A21: ( n in dom f & m in dom f ) and A22: n < m ; ::_thesis: ( f /. n <> f /. m & [(f /. n),(f /. m)] in RealOrd ) A23: ( 1 <= n & m <= width G ) by A3, A21, FINSEQ_3:25; reconsider n9 = n, m9 = m as Element of NAT by ORDINAL1:def_12; A24: ( f /. n = f . n & f /. m = f . m ) by A21, PARTFUN1:def_6; A25: ( f . n = (G * (1,n9)) `2 & f . m = (G * (1,m9)) `2 ) by A4, A21; hence f /. n <> f /. m by A2, A22, A23, A24, GOBOARD5:4; ::_thesis: [(f /. n),(f /. m)] in RealOrd f . n9 < f . m9 by A2, A22, A25, A23, GOBOARD5:4; hence [(f /. n),(f /. m)] in RealOrd by A24; ::_thesis: verum end; then f = SgmX (RealOrd,(proj2 .: (Values G))) by A6, PRE_POLY:9; hence (SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2 by A4, A5, A1; ::_thesis: verum end; theorem Th30: :: JORDAN1H:30 for f being non empty FinSequence of (TOP-REAL 2) for G being Go-board st f is_sequence_on G & ex i being Element of NAT st ( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st ( [(len G),i] in Indices G & G * ((len G),i) in rng f ) holds proj1 .: (rng f) = proj1 .: (Values G) proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board st f is_sequence_on G & ex i being Element of NAT st ( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st ( [(len G),i] in Indices G & G * ((len G),i) in rng f ) holds proj1 .: (rng f) = proj1 .: (Values G) let G be Go-board; ::_thesis: ( f is_sequence_on G & ex i being Element of NAT st ( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st ( [(len G),i] in Indices G & G * ((len G),i) in rng f ) implies proj1 .: (rng f) = proj1 .: (Values G) ) assume A1: f is_sequence_on G ; ::_thesis: ( for i being Element of NAT holds ( not [1,i] in Indices G or not G * (1,i) in rng f ) or for i being Element of NAT holds ( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or proj1 .: (rng f) = proj1 .: (Values G) ) given i1 being Element of NAT such that A2: [1,i1] in Indices G and A3: G * (1,i1) in rng f ; ::_thesis: ( for i being Element of NAT holds ( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or proj1 .: (rng f) = proj1 .: (Values G) ) consider k1 being set such that A4: k1 in dom f and A5: G * (1,i1) = f . k1 by A3, FUNCT_1:def_3; reconsider k1 = k1 as Element of NAT by A4; A6: 1 <= k1 by A4, FINSEQ_3:25; given i2 being Element of NAT such that A7: [(len G),i2] in Indices G and A8: G * ((len G),i2) in rng f ; ::_thesis: proj1 .: (rng f) = proj1 .: (Values G) consider k2 being set such that A9: k2 in dom f and A10: G * ((len G),i2) = f . k2 by A8, FUNCT_1:def_3; reconsider k2 = k2 as Element of NAT by A9; A11: k2 <= len f by A9, FINSEQ_3:25; A12: k1 <= len f by A4, FINSEQ_3:25; set g = mid (f,k1,k2); A13: mid (f,k1,k2) is_sequence_on G by A1, Th27; A14: 1 <= k2 by A9, FINSEQ_3:25; A15: now__::_thesis:_len_(mid_(f,k1,k2))_>=_0_+_1 percases ( k1 <= k2 or k1 > k2 ) ; suppose k1 <= k2 ; ::_thesis: len (mid (f,k1,k2)) >= 0 + 1 then len (mid (f,k1,k2)) = (k2 -' k1) + 1 by A6, A11, JORDAN4:8; hence len (mid (f,k1,k2)) >= 0 + 1 by XREAL_1:6; ::_thesis: verum end; suppose k1 > k2 ; ::_thesis: len (mid (f,k1,k2)) >= 0 + 1 then len (mid (f,k1,k2)) = (k1 -' k2) + 1 by A12, A14, JORDAN4:9; hence len (mid (f,k1,k2)) >= 0 + 1 by XREAL_1:6; ::_thesis: verum end; end; end; A16: Values G = { (G * (i,j)) where i, j is Element of NAT : [i,j] in Indices G } by MATRIX_1:45; A17: proj1 .: (Values G) c= proj1 .: (rng (mid (f,k1,k2))) proof assume not proj1 .: (Values G) c= proj1 .: (rng (mid (f,k1,k2))) ; ::_thesis: contradiction then consider x being Element of REAL such that A18: x in proj1 .: (Values G) and A19: not x in proj1 .: (rng (mid (f,k1,k2))) by SUBSET_1:2; consider p being Element of (TOP-REAL 2) such that A20: p in Values G and A21: x = proj1 . p by A18, FUNCT_2:65; consider i0, j0 being Element of NAT such that A22: p = G * (i0,j0) and A23: [i0,j0] in Indices G by A16, A20; A24: i0 <= len G by A23, MATRIX_1:38; defpred S1[ Nat] means ( 1 <= $1 & $1 <= len (mid (f,k1,k2)) implies for i, j being Element of NAT st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . $1 holds i < i0 ); A25: 1 <= i0 by A23, MATRIX_1:38; A26: ( 1 <= j0 & j0 <= width G ) by A23, MATRIX_1:38; A27: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume that A28: ( 1 <= n & n <= len (mid (f,k1,k2)) implies for i, j being Element of NAT st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . n holds i < i0 ) and A29: 1 <= n + 1 and A30: n + 1 <= len (mid (f,k1,k2)) ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . (n + 1) holds i < i0 let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . (n + 1) implies i < i0 ) assume that A31: [i,j] in Indices G and A32: G * (i,j) = (mid (f,k1,k2)) . (n + 1) ; ::_thesis: i < i0 A33: now__::_thesis:_not_i_=_i0 A34: n + 1 in dom (mid (f,k1,k2)) by A29, A30, FINSEQ_3:25; then A35: G * (i,j) = (mid (f,k1,k2)) /. (n + 1) by A32, PARTFUN1:def_6; then A36: ( dom proj1 = the carrier of (TOP-REAL 2) & (mid (f,k1,k2)) /. (n + 1) in rng (mid (f,k1,k2)) ) by A32, A34, FUNCT_1:3, FUNCT_2:def_1; A37: ( 1 <= j & j <= width G ) by A31, MATRIX_1:38; assume A38: i = i0 ; ::_thesis: contradiction x = p `1 by A21, PSCOMP_1:def_5 .= (G * (i0,1)) `1 by A22, A25, A24, A26, GOBOARD5:2 .= (G * (i,j)) `1 by A25, A24, A38, A37, GOBOARD5:2 .= proj1 . ((mid (f,k1,k2)) /. (n + 1)) by A35, PSCOMP_1:def_5 ; hence contradiction by A19, A36, FUNCT_1:def_6; ::_thesis: verum end; percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: i < i0 then G * (i,j) = G * (1,i1) by A5, A6, A12, A14, A11, A32, FINSEQ_6:118; then i = 1 by A2, A31, Th26; hence i < i0 by A25, A33, XXREAL_0:1; ::_thesis: verum end; supposeA39: n <> 0 ; ::_thesis: i < i0 then A40: 1 <= n by NAT_1:14; A41: n <= n + 1 by NAT_1:11; then n <= len (mid (f,k1,k2)) by A30, XXREAL_0:2; then A42: n in dom (mid (f,k1,k2)) by A40, FINSEQ_3:25; then consider i1, j1 being Element of NAT such that A43: ( [i1,j1] in Indices G & (mid (f,k1,k2)) /. n = G * (i1,j1) ) by A13, GOBOARD1:def_9; A44: n + 1 in dom (mid (f,k1,k2)) by A29, A30, FINSEQ_3:25; then (mid (f,k1,k2)) /. (n + 1) = G * (i,j) by A32, PARTFUN1:def_6; then (abs (i1 - i)) + (abs (j1 - j)) = 1 by A13, A31, A42, A43, A44, GOBOARD1:def_9; then A45: ( ( abs (i1 - i) = 1 & j1 = j ) or ( abs (j1 - j) = 1 & i1 = i ) ) by SEQM_3:42; now__::_thesis:_i_<_i0 (mid (f,k1,k2)) . n = (mid (f,k1,k2)) /. n by A42, PARTFUN1:def_6; then A46: i1 < i0 by A28, A30, A39, A41, A43, NAT_1:14, XXREAL_0:2; percases ( i1 = i or i < i1 or i = i1 + 1 ) by A45, SEQM_3:41; suppose ( i1 = i or i < i1 ) ; ::_thesis: i < i0 hence i < i0 by A46, XXREAL_0:2; ::_thesis: verum end; suppose i = i1 + 1 ; ::_thesis: i < i0 then i <= i0 by A46, NAT_1:13; hence i < i0 by A33, XXREAL_0:1; ::_thesis: verum end; end; end; hence i < i0 ; ::_thesis: verum end; end; end; A47: G * ((len G),i2) = (mid (f,k1,k2)) . (len (mid (f,k1,k2))) by A6, A12, A10, A14, A11, JORDAN4:11; A48: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A48, A27); then len G < i0 by A7, A15, A47; hence contradiction by A23, MATRIX_1:38; ::_thesis: verum end; thus proj1 .: (rng f) c= proj1 .: (Values G) by A1, GOBRD13:8, RELAT_1:123; :: according to XBOOLE_0:def_10 ::_thesis: proj1 .: (Values G) c= proj1 .: (rng f) proj1 .: (rng (mid (f,k1,k2))) c= proj1 .: (rng f) by FINSEQ_6:119, RELAT_1:123; hence proj1 .: (Values G) c= proj1 .: (rng f) by A17, XBOOLE_1:1; ::_thesis: verum end; theorem Th31: :: JORDAN1H:31 for f being non empty FinSequence of (TOP-REAL 2) for G being Go-board st f is_sequence_on G & ex i being Element of NAT st ( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st ( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds proj2 .: (rng f) = proj2 .: (Values G) proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board st f is_sequence_on G & ex i being Element of NAT st ( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st ( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds proj2 .: (rng f) = proj2 .: (Values G) let G be Go-board; ::_thesis: ( f is_sequence_on G & ex i being Element of NAT st ( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st ( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) implies proj2 .: (rng f) = proj2 .: (Values G) ) assume A1: f is_sequence_on G ; ::_thesis: ( for i being Element of NAT holds ( not [i,1] in Indices G or not G * (i,1) in rng f ) or for i being Element of NAT holds ( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or proj2 .: (rng f) = proj2 .: (Values G) ) given i1 being Element of NAT such that A2: [i1,1] in Indices G and A3: G * (i1,1) in rng f ; ::_thesis: ( for i being Element of NAT holds ( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or proj2 .: (rng f) = proj2 .: (Values G) ) consider k1 being set such that A4: k1 in dom f and A5: G * (i1,1) = f . k1 by A3, FUNCT_1:def_3; reconsider k1 = k1 as Element of NAT by A4; A6: 1 <= k1 by A4, FINSEQ_3:25; given i2 being Element of NAT such that A7: [i2,(width G)] in Indices G and A8: G * (i2,(width G)) in rng f ; ::_thesis: proj2 .: (rng f) = proj2 .: (Values G) consider k2 being set such that A9: k2 in dom f and A10: G * (i2,(width G)) = f . k2 by A8, FUNCT_1:def_3; reconsider k2 = k2 as Element of NAT by A9; A11: k2 <= len f by A9, FINSEQ_3:25; A12: k1 <= len f by A4, FINSEQ_3:25; set g = mid (f,k1,k2); A13: mid (f,k1,k2) is_sequence_on G by A1, Th27; A14: 1 <= k2 by A9, FINSEQ_3:25; A15: now__::_thesis:_len_(mid_(f,k1,k2))_>=_0_+_1 percases ( k1 <= k2 or k1 > k2 ) ; suppose k1 <= k2 ; ::_thesis: len (mid (f,k1,k2)) >= 0 + 1 then len (mid (f,k1,k2)) = (k2 -' k1) + 1 by A6, A11, JORDAN4:8; hence len (mid (f,k1,k2)) >= 0 + 1 by XREAL_1:6; ::_thesis: verum end; suppose k1 > k2 ; ::_thesis: len (mid (f,k1,k2)) >= 0 + 1 then len (mid (f,k1,k2)) = (k1 -' k2) + 1 by A12, A14, JORDAN4:9; hence len (mid (f,k1,k2)) >= 0 + 1 by XREAL_1:6; ::_thesis: verum end; end; end; A16: Values G = { (G * (i,j)) where i, j is Element of NAT : [i,j] in Indices G } by MATRIX_1:45; A17: proj2 .: (Values G) c= proj2 .: (rng (mid (f,k1,k2))) proof assume not proj2 .: (Values G) c= proj2 .: (rng (mid (f,k1,k2))) ; ::_thesis: contradiction then consider x being Element of REAL such that A18: x in proj2 .: (Values G) and A19: not x in proj2 .: (rng (mid (f,k1,k2))) by SUBSET_1:2; consider p being Element of (TOP-REAL 2) such that A20: p in Values G and A21: x = proj2 . p by A18, FUNCT_2:65; consider i0, j0 being Element of NAT such that A22: p = G * (i0,j0) and A23: [i0,j0] in Indices G by A16, A20; A24: j0 <= width G by A23, MATRIX_1:38; defpred S1[ Nat] means ( 1 <= $1 & $1 <= len (mid (f,k1,k2)) implies for i, j being Element of NAT st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . $1 holds j < j0 ); A25: 1 <= j0 by A23, MATRIX_1:38; A26: ( 1 <= i0 & i0 <= len G ) by A23, MATRIX_1:38; A27: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume that A28: ( 1 <= n & n <= len (mid (f,k1,k2)) implies for i, j being Element of NAT st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . n holds j < j0 ) and A29: 1 <= n + 1 and A30: n + 1 <= len (mid (f,k1,k2)) ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . (n + 1) holds j < j0 let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices G & G * (i,j) = (mid (f,k1,k2)) . (n + 1) implies j < j0 ) assume that A31: [i,j] in Indices G and A32: G * (i,j) = (mid (f,k1,k2)) . (n + 1) ; ::_thesis: j < j0 A33: now__::_thesis:_not_j_=_j0 A34: n + 1 in dom (mid (f,k1,k2)) by A29, A30, FINSEQ_3:25; then A35: G * (i,j) = (mid (f,k1,k2)) /. (n + 1) by A32, PARTFUN1:def_6; then A36: ( dom proj2 = the carrier of (TOP-REAL 2) & (mid (f,k1,k2)) /. (n + 1) in rng (mid (f,k1,k2)) ) by A32, A34, FUNCT_1:3, FUNCT_2:def_1; A37: ( 1 <= i & i <= len G ) by A31, MATRIX_1:38; assume A38: j = j0 ; ::_thesis: contradiction x = p `2 by A21, PSCOMP_1:def_6 .= (G * (1,j0)) `2 by A22, A26, A25, A24, GOBOARD5:1 .= (G * (i,j)) `2 by A25, A24, A38, A37, GOBOARD5:1 .= proj2 . ((mid (f,k1,k2)) /. (n + 1)) by A35, PSCOMP_1:def_6 ; hence contradiction by A19, A36, FUNCT_1:def_6; ::_thesis: verum end; percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: j < j0 then G * (i,j) = G * (i1,1) by A5, A6, A12, A14, A11, A32, FINSEQ_6:118; then j = 1 by A2, A31, Th26; hence j < j0 by A25, A33, XXREAL_0:1; ::_thesis: verum end; supposeA39: n <> 0 ; ::_thesis: j < j0 then A40: 1 <= n by NAT_1:14; A41: n <= n + 1 by NAT_1:11; then n <= len (mid (f,k1,k2)) by A30, XXREAL_0:2; then A42: n in dom (mid (f,k1,k2)) by A40, FINSEQ_3:25; then consider i1, j1 being Element of NAT such that A43: ( [i1,j1] in Indices G & (mid (f,k1,k2)) /. n = G * (i1,j1) ) by A13, GOBOARD1:def_9; A44: n + 1 in dom (mid (f,k1,k2)) by A29, A30, FINSEQ_3:25; then (mid (f,k1,k2)) /. (n + 1) = G * (i,j) by A32, PARTFUN1:def_6; then (abs (i1 - i)) + (abs (j1 - j)) = 1 by A13, A31, A42, A43, A44, GOBOARD1:def_9; then A45: ( ( abs (i1 - i) = 1 & j1 = j ) or ( abs (j1 - j) = 1 & i1 = i ) ) by SEQM_3:42; now__::_thesis:_j_<_j0 (mid (f,k1,k2)) . n = (mid (f,k1,k2)) /. n by A42, PARTFUN1:def_6; then A46: j1 < j0 by A28, A30, A39, A41, A43, NAT_1:14, XXREAL_0:2; percases ( j1 = j or j < j1 or j = j1 + 1 ) by A45, SEQM_3:41; suppose ( j1 = j or j < j1 ) ; ::_thesis: j < j0 hence j < j0 by A46, XXREAL_0:2; ::_thesis: verum end; suppose j = j1 + 1 ; ::_thesis: j < j0 then j <= j0 by A46, NAT_1:13; hence j < j0 by A33, XXREAL_0:1; ::_thesis: verum end; end; end; hence j < j0 ; ::_thesis: verum end; end; end; A47: G * (i2,(width G)) = (mid (f,k1,k2)) . (len (mid (f,k1,k2))) by A6, A12, A10, A14, A11, JORDAN4:11; A48: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A48, A27); then width G < j0 by A7, A15, A47; hence contradiction by A23, MATRIX_1:38; ::_thesis: verum end; thus proj2 .: (rng f) c= proj2 .: (Values G) by A1, GOBRD13:8, RELAT_1:123; :: according to XBOOLE_0:def_10 ::_thesis: proj2 .: (Values G) c= proj2 .: (rng f) proj2 .: (rng (mid (f,k1,k2))) c= proj2 .: (rng f) by FINSEQ_6:119, RELAT_1:123; hence proj2 .: (Values G) c= proj2 .: (rng f) by A17, XBOOLE_1:1; ::_thesis: verum end; registration let G be Go-board; cluster Values G -> non empty ; coherence not Values G is empty proof not dom G is empty ; then reconsider f = rngs G as non empty non-empty Function by FUNCT_6:60, RELAT_1:38; not Union f is empty ; hence not Values G is empty by MATRIX_1:def_16; ::_thesis: verum end; end; theorem Th32: :: JORDAN1H:32 for G being Go-board holds G = GoB ((SgmX (RealOrd,(proj1 .: (Values G)))),(SgmX (RealOrd,(proj2 .: (Values G))))) proof let G be Go-board; ::_thesis: G = GoB ((SgmX (RealOrd,(proj1 .: (Values G)))),(SgmX (RealOrd,(proj2 .: (Values G))))) set v1 = SgmX (RealOrd,(proj1 .: (Values G))); set v2 = SgmX (RealOrd,(proj2 .: (Values G))); A1: width G = card (proj2 .: (Values G)) by Th19 .= len (SgmX (RealOrd,(proj2 .: (Values G)))) by Th9 ; A2: for n, m being Element of NAT st [n,m] in Indices G holds G * (n,m) = |[((SgmX (RealOrd,(proj1 .: (Values G)))) . n),((SgmX (RealOrd,(proj2 .: (Values G)))) . m)]| proof let n, m be Element of NAT ; ::_thesis: ( [n,m] in Indices G implies G * (n,m) = |[((SgmX (RealOrd,(proj1 .: (Values G)))) . n),((SgmX (RealOrd,(proj2 .: (Values G)))) . m)]| ) assume A3: [n,m] in Indices G ; ::_thesis: G * (n,m) = |[((SgmX (RealOrd,(proj1 .: (Values G)))) . n),((SgmX (RealOrd,(proj2 .: (Values G)))) . m)]| then A4: ( 1 <= n & n <= len G ) by MATRIX_1:38; A5: ( 1 <= m & m <= width G ) by A3, MATRIX_1:38; (SgmX (RealOrd,(proj1 .: (Values G)))) . n = (G * (n,1)) `1 by A4, Th28; then A6: (SgmX (RealOrd,(proj1 .: (Values G)))) . n = (G * (n,m)) `1 by A4, A5, GOBOARD5:2; (SgmX (RealOrd,(proj2 .: (Values G)))) . m = (G * (1,m)) `2 by A5, Th29; then (SgmX (RealOrd,(proj2 .: (Values G)))) . m = (G * (n,m)) `2 by A4, A5, GOBOARD5:1; hence G * (n,m) = |[((SgmX (RealOrd,(proj1 .: (Values G)))) . n),((SgmX (RealOrd,(proj2 .: (Values G)))) . m)]| by A6, EUCLID:53; ::_thesis: verum end; len G = card (proj1 .: (Values G)) by Th16 .= len (SgmX (RealOrd,(proj1 .: (Values G)))) by Th9 ; hence G = GoB ((SgmX (RealOrd,(proj1 .: (Values G)))),(SgmX (RealOrd,(proj2 .: (Values G))))) by A1, A2, GOBOARD2:def_1; ::_thesis: verum end; theorem Th33: :: JORDAN1H:33 for f being non empty FinSequence of (TOP-REAL 2) for G being Go-board st proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) holds G = GoB f proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board st proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) holds G = GoB f let G be Go-board; ::_thesis: ( proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) implies G = GoB f ) X_axis f = proj1 * f by Th10; then rng (X_axis f) = proj1 .: (rng f) by RELAT_1:127; then A1: Incr (X_axis f) = SgmX (RealOrd,(proj1 .: (rng f))) by Th8; Y_axis f = proj2 * f by Th11; then rng (Y_axis f) = proj2 .: (rng f) by RELAT_1:127; then A2: Incr (Y_axis f) = SgmX (RealOrd,(proj2 .: (rng f))) by Th8; assume ( proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) ) ; ::_thesis: G = GoB f hence G = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by A1, A2, Th32 .= GoB f by GOBOARD2:def_2 ; ::_thesis: verum end; theorem Th34: :: JORDAN1H:34 for f being non empty FinSequence of (TOP-REAL 2) for G being Go-board st f is_sequence_on G & ex i being Element of NAT st ( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st ( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st ( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Element of NAT st ( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds G = GoB f proof let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board st f is_sequence_on G & ex i being Element of NAT st ( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st ( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st ( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Element of NAT st ( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds G = GoB f let G be Go-board; ::_thesis: ( f is_sequence_on G & ex i being Element of NAT st ( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Element of NAT st ( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Element of NAT st ( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Element of NAT st ( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) implies G = GoB f ) assume A1: f is_sequence_on G ; ::_thesis: ( for i being Element of NAT holds ( not [1,i] in Indices G or not G * (1,i) in rng f ) or for i being Element of NAT holds ( not [i,1] in Indices G or not G * (i,1) in rng f ) or for i being Element of NAT holds ( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or for i being Element of NAT holds ( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or G = GoB f ) given i1 being Element of NAT such that A2: ( [1,i1] in Indices G & G * (1,i1) in rng f ) ; ::_thesis: ( for i being Element of NAT holds ( not [i,1] in Indices G or not G * (i,1) in rng f ) or for i being Element of NAT holds ( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or for i being Element of NAT holds ( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or G = GoB f ) given i2 being Element of NAT such that A3: ( [i2,1] in Indices G & G * (i2,1) in rng f ) ; ::_thesis: ( for i being Element of NAT holds ( not [(len G),i] in Indices G or not G * ((len G),i) in rng f ) or for i being Element of NAT holds ( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or G = GoB f ) given i3 being Element of NAT such that A4: ( [(len G),i3] in Indices G & G * ((len G),i3) in rng f ) ; ::_thesis: ( for i being Element of NAT holds ( not [i,(width G)] in Indices G or not G * (i,(width G)) in rng f ) or G = GoB f ) given i4 being Element of NAT such that A5: ( [i4,(width G)] in Indices G & G * (i4,(width G)) in rng f ) ; ::_thesis: G = GoB f A6: proj2 .: (rng f) = proj2 .: (Values G) by A1, A3, A5, Th31; proj1 .: (rng f) = proj1 .: (Values G) by A1, A2, A4, Th30; hence G = GoB f by A6, Th33; ::_thesis: verum end; begin theorem Th35: :: JORDAN1H:35 for i, n, m being Element of NAT st 1 <= i holds [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT proof let i, n, m be Element of NAT ; ::_thesis: ( 1 <= i implies [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT ) set i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/]; (((i - 2) / (2 |^ (n -' m))) + 2) - 1 = ((i - 2) / (2 |^ (n -' m))) + (2 - 1) ; then A1: ((i - 2) / (2 |^ (n -' m))) + 1 < [\(((i - 2) / (2 |^ (n -' m))) + 2)/] by INT_1:def_6; ( (n -' m) + 1 >= 0 + 1 & (n -' m) + 1 <= 2 |^ (n -' m) ) by NEWTON:85, XREAL_1:6; then 0 + 1 <= 2 |^ (n -' m) by XXREAL_0:2; then A2: (- 1) / 1 <= (- 1) / (2 |^ (n -' m)) by XREAL_1:120; assume 1 <= i ; ::_thesis: [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT then 1 - 2 <= i - 2 by XREAL_1:9; then (- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:72; then - 1 <= (i - 2) / (2 |^ (n -' m)) by A2, XXREAL_0:2; then (- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:6; hence [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT by A1, INT_1:3; ::_thesis: verum end; theorem Th36: :: JORDAN1H:36 for m, n, i being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) holds ( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) ) proof let m, n, i be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) holds ( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) ) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) implies ( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) ) ) assume that A1: m <= n and A2: 1 <= i and A3: i + 1 <= len (Gauge (C,n)) ; ::_thesis: ( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) ) A4: (n -' m) + 1 <= 2 |^ (n -' m) by NEWTON:85; i + 1 <= (2 |^ n) + (2 + 1) by A3, JORDAN8:def_1; then i + 1 <= ((2 |^ n) + 2) + 1 ; then i <= (2 |^ n) + 2 by XREAL_1:6; then i - 2 <= 2 |^ n by XREAL_1:20; then i - 2 <= 2 |^ (m + (n -' m)) by A1, XREAL_1:235; then (i - 2) * 1 <= (2 |^ m) * (2 |^ (n -' m)) by NEWTON:8; then (i - 2) / (2 |^ (n -' m)) <= (2 |^ m) / 1 by A4, XREAL_1:102; then ((i - 2) / (2 |^ (n -' m))) + 3 <= (2 |^ m) + 3 by XREAL_1:6; then A5: ((i - 2) / (2 |^ (n -' m))) + 3 <= len (Gauge (C,m)) by JORDAN8:def_1; set i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/]; (((i - 2) / (2 |^ (n -' m))) + 2) - 1 = ((i - 2) / (2 |^ (n -' m))) + (2 - 1) ; then A6: ((i - 2) / (2 |^ (n -' m))) + 1 < [\(((i - 2) / (2 |^ (n -' m))) + 2)/] by INT_1:def_6; (n -' m) + 1 >= 0 + 1 by XREAL_1:6; then 0 + 1 <= 2 |^ (n -' m) by A4, XXREAL_0:2; then A7: (- 1) / 1 <= (- 1) / (2 |^ (n -' m)) by XREAL_1:120; 1 - 2 <= i - 2 by A2, XREAL_1:9; then (- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:72; then - 1 <= (i - 2) / (2 |^ (n -' m)) by A7, XXREAL_0:2; then (- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:6; then [\(((i - 2) / (2 |^ (n -' m))) + 2)/] >= 1 + 0 by A6, INT_1:7; hence 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] ; ::_thesis: [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) [\(((i - 2) / (2 |^ (n -' m))) + 2)/] <= ((i - 2) / (2 |^ (n -' m))) + 2 by INT_1:def_6; then [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= (((i - 2) / (2 |^ (n -' m))) + 2) + 1 by XREAL_1:6; hence [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) by A5, XXREAL_0:2; ::_thesis: verum end; theorem Th37: :: JORDAN1H:37 for m, n, i, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds ex i1, j1 being Element of NAT st ( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) proof let m, n, i, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds ex i1, j1 being Element of NAT st ( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) implies ex i1, j1 being Element of NAT st ( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) ) assume that A1: m <= n and A2: 1 <= i and A3: i + 1 <= len (Gauge (C,n)) and A4: 1 <= j and A5: j + 1 <= width (Gauge (C,n)) ; ::_thesis: ex i1, j1 being Element of NAT st ( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) reconsider i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/], j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] as Element of NAT by A2, A4, Th35; set Gm = Gauge (C,m); set Gn = Gauge (C,n); A6: 2 |^ (n -' m) > n -' m by NEWTON:86; take i1 ; ::_thesis: ex j1 being Element of NAT st ( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) take j1 ; ::_thesis: ( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) thus i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] ; ::_thesis: ( j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) thus j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] ; ::_thesis: cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in cell ((Gauge (C,n)),i,j) or e in cell ((Gauge (C,m)),i1,j1) ) assume A7: e in cell ((Gauge (C,n)),i,j) ; ::_thesis: e in cell ((Gauge (C,m)),i1,j1) then reconsider p = e as Point of (TOP-REAL 2) ; A8: p `2 <= ((Gauge (C,n)) * (i,(j + 1))) `2 by A2, A3, A4, A5, A7, JORDAN9:17; ( i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) ) by A3, A5, NAT_1:13; then [i,j] in Indices (Gauge (C,n)) by A2, A4, MATRIX_1:36; then A9: (Gauge (C,n)) * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by JORDAN8:def_1; then A10: ((Gauge (C,n)) * (i,j)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((i - 2) / 1)) by EUCLID:52 .= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * ((i - 2) / (2 |^ n))) by XCMPLX_1:85 ; A11: ((Gauge (C,n)) * (i,j)) `1 <= p `1 by A2, A3, A4, A5, A7, JORDAN9:17; A12: ((Gauge (C,n)) * (i,j)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((j - 2) / 1)) by A9, EUCLID:52 .= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * ((j - 2) / (2 |^ n))) by XCMPLX_1:85 ; A13: p `1 <= ((Gauge (C,n)) * ((i + 1),j)) `1 by A2, A3, A4, A5, A7, JORDAN9:17; E-bound C >= (W-bound C) + 0 by SPRECT_1:21; then A14: (E-bound C) - (W-bound C) >= 0 by XREAL_1:19; ( 1 <= j + 1 & i <= len (Gauge (C,n)) ) by A3, NAT_1:11, NAT_1:13; then [i,(j + 1)] in Indices (Gauge (C,n)) by A2, A5, MATRIX_1:36; then (Gauge (C,n)) * (i,(j + 1)) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((j + 1) - 2)))]| by JORDAN8:def_1; then A15: ((Gauge (C,n)) * (i,(j + 1))) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((j + 1) - 2) / 1)) by EUCLID:52 .= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * (((j + 1) - 2) / (2 |^ n))) by XCMPLX_1:85 ; ( (n -' m) + 1 >= 0 + 1 & (n -' m) + 1 <= 2 |^ (n -' m) ) by NEWTON:85, XREAL_1:6; then 0 + 1 <= 2 |^ (n -' m) by XXREAL_0:2; then A16: (- 1) / 1 <= (- 1) / (2 |^ (n -' m)) by XREAL_1:120; A17: ((Gauge (C,n)) * (i,j)) `2 <= p `2 by A2, A3, A4, A5, A7, JORDAN9:17; ( 1 <= i + 1 & j <= width (Gauge (C,n)) ) by A5, NAT_1:11, NAT_1:13; then [(i + 1),j] in Indices (Gauge (C,n)) by A3, A4, MATRIX_1:36; then (Gauge (C,n)) * ((i + 1),j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((i + 1) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by JORDAN8:def_1; then A18: ((Gauge (C,n)) * ((i + 1),j)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (((i + 1) - 2) / 1)) by EUCLID:52 .= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * (((i + 1) - 2) / (2 |^ n))) by XCMPLX_1:85 ; (((i - 2) / (2 |^ (n -' m))) + 2) - 1 = ((i - 2) / (2 |^ (n -' m))) + (2 - 1) ; then A19: ((i - 2) / (2 |^ (n -' m))) + 1 < i1 by INT_1:def_6; 1 - 2 <= i - 2 by A2, XREAL_1:9; then (- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:72; then - 1 <= (i - 2) / (2 |^ (n -' m)) by A16, XXREAL_0:2; then (- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:6; then A20: i1 >= 1 + 0 by A19, INT_1:7; N-bound C >= (S-bound C) + 0 by SPRECT_1:22; then A21: (N-bound C) - (S-bound C) >= 0 by XREAL_1:19; (((i - 2) / (2 |^ (n -' m))) + 2) - 1 < i1 by INT_1:def_6; then ((i - 2) / (2 |^ (n -' m))) + 2 < i1 + 1 by XREAL_1:19; then (i - 2) / (2 |^ (n -' m)) < (i1 + 1) - 2 by XREAL_1:20; then (i - 2) + 1 <= ((i1 + 1) - 2) * (2 |^ (n -' m)) by A6, INT_1:7, XREAL_1:77; then ((i + 1) - 2) / (2 |^ (n -' m)) <= (i1 + 1) - 2 by A6, XREAL_1:79; then (((i + 1) - 2) / (2 |^ (n -' m))) / (2 |^ m) <= ((i1 + 1) - 2) / (2 |^ m) by XREAL_1:72; then ((i + 1) - 2) / ((2 |^ (n -' m)) * (2 |^ m)) <= ((i1 + 1) - 2) / (2 |^ m) by XCMPLX_1:78; then ((i + 1) - 2) / (2 |^ ((n -' m) + m)) <= ((i1 + 1) - 2) / (2 |^ m) by NEWTON:8; then ((i + 1) - 2) / (2 |^ n) <= ((i1 + 1) - 2) / (2 |^ m) by A1, XREAL_1:235; then A22: ((E-bound C) - (W-bound C)) * (((i + 1) - 2) / (2 |^ n)) <= ((E-bound C) - (W-bound C)) * (((i1 + 1) - 2) / (2 |^ m)) by A14, XREAL_1:64; i1 <= ((i - 2) / (2 |^ (n -' m))) + 2 by INT_1:def_6; then i1 - 2 <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:20; then (i1 - 2) / (2 |^ m) <= ((i - 2) / (2 |^ (n -' m))) / (2 |^ m) by XREAL_1:72; then (i1 - 2) / (2 |^ m) <= (i - 2) / ((2 |^ (n -' m)) * (2 |^ m)) by XCMPLX_1:78; then (i1 - 2) / (2 |^ m) <= (i - 2) / (2 |^ ((n -' m) + m)) by NEWTON:8; then (i1 - 2) / (2 |^ m) <= (i - 2) / (2 |^ n) by A1, XREAL_1:235; then A23: ((E-bound C) - (W-bound C)) * ((i1 - 2) / (2 |^ m)) <= ((E-bound C) - (W-bound C)) * ((i - 2) / (2 |^ n)) by A14, XREAL_1:64; j1 <= ((j - 2) / (2 |^ (n -' m))) + 2 by INT_1:def_6; then j1 - 2 <= (j - 2) / (2 |^ (n -' m)) by XREAL_1:20; then (j1 - 2) / (2 |^ m) <= ((j - 2) / (2 |^ (n -' m))) / (2 |^ m) by XREAL_1:72; then (j1 - 2) / (2 |^ m) <= (j - 2) / ((2 |^ (n -' m)) * (2 |^ m)) by XCMPLX_1:78; then (j1 - 2) / (2 |^ m) <= (j - 2) / (2 |^ ((n -' m) + m)) by NEWTON:8; then (j1 - 2) / (2 |^ m) <= (j - 2) / (2 |^ n) by A1, XREAL_1:235; then A24: ((N-bound C) - (S-bound C)) * ((j1 - 2) / (2 |^ m)) <= ((N-bound C) - (S-bound C)) * ((j - 2) / (2 |^ n)) by A21, XREAL_1:64; (((j - 2) / (2 |^ (n -' m))) + 2) - 1 = ((j - 2) / (2 |^ (n -' m))) + (2 - 1) ; then A25: ((j - 2) / (2 |^ (n -' m))) + 1 < j1 by INT_1:def_6; 1 - 2 <= j - 2 by A4, XREAL_1:9; then (- 1) / (2 |^ (n -' m)) <= (j - 2) / (2 |^ (n -' m)) by XREAL_1:72; then - 1 <= (j - 2) / (2 |^ (n -' m)) by A16, XXREAL_0:2; then (- 1) + 1 <= ((j - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:6; then A26: j1 >= 1 + 0 by A25, INT_1:7; (((j - 2) / (2 |^ (n -' m))) + 2) - 1 < j1 by INT_1:def_6; then ((j - 2) / (2 |^ (n -' m))) + 2 < j1 + 1 by XREAL_1:19; then (j - 2) / (2 |^ (n -' m)) < (j1 + 1) - 2 by XREAL_1:20; then (j - 2) + 1 <= ((j1 + 1) - 2) * (2 |^ (n -' m)) by A6, INT_1:7, XREAL_1:77; then ((j + 1) - 2) / (2 |^ (n -' m)) <= (j1 + 1) - 2 by A6, XREAL_1:79; then (((j + 1) - 2) / (2 |^ (n -' m))) / (2 |^ m) <= ((j1 + 1) - 2) / (2 |^ m) by XREAL_1:72; then ((j + 1) - 2) / ((2 |^ (n -' m)) * (2 |^ m)) <= ((j1 + 1) - 2) / (2 |^ m) by XCMPLX_1:78; then ((j + 1) - 2) / (2 |^ ((n -' m) + m)) <= ((j1 + 1) - 2) / (2 |^ m) by NEWTON:8; then ((j + 1) - 2) / (2 |^ n) <= ((j1 + 1) - 2) / (2 |^ m) by A1, XREAL_1:235; then A27: ((N-bound C) - (S-bound C)) * (((j + 1) - 2) / (2 |^ n)) <= ((N-bound C) - (S-bound C)) * (((j1 + 1) - 2) / (2 |^ m)) by A21, XREAL_1:64; ( len (Gauge (C,m)) = width (Gauge (C,m)) & len (Gauge (C,n)) = width (Gauge (C,n)) ) by JORDAN8:def_1; then A28: j1 + 1 <= width (Gauge (C,m)) by A1, A4, A5, Th36; then A29: j1 <= width (Gauge (C,m)) by NAT_1:13; A30: i1 + 1 <= len (Gauge (C,m)) by A1, A2, A3, Th36; then ( 1 <= j1 + 1 & i1 <= len (Gauge (C,m)) ) by NAT_1:11, NAT_1:13; then [i1,(j1 + 1)] in Indices (Gauge (C,m)) by A20, A28, MATRIX_1:36; then (Gauge (C,m)) * (i1,(j1 + 1)) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * ((j1 + 1) - 2)))]| by JORDAN8:def_1; then ((Gauge (C,m)) * (i1,(j1 + 1))) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * (((j1 + 1) - 2) / 1)) by EUCLID:52 .= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * (((j1 + 1) - 2) / (2 |^ m))) by XCMPLX_1:85 ; then ((Gauge (C,n)) * (i,(j + 1))) `2 <= ((Gauge (C,m)) * (i1,(j1 + 1))) `2 by A15, A27, XREAL_1:6; then A31: p `2 <= ((Gauge (C,m)) * (i1,(j1 + 1))) `2 by A8, XXREAL_0:2; i1 <= len (Gauge (C,m)) by A30, NAT_1:13; then [i1,j1] in Indices (Gauge (C,m)) by A20, A26, A29, MATRIX_1:36; then A32: (Gauge (C,m)) * (i1,j1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * (j1 - 2)))]| by JORDAN8:def_1; then ((Gauge (C,m)) * (i1,j1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * ((i1 - 2) / 1)) by EUCLID:52 .= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * ((i1 - 2) / (2 |^ m))) by XCMPLX_1:85 ; then ((Gauge (C,m)) * (i1,j1)) `1 <= ((Gauge (C,n)) * (i,j)) `1 by A10, A23, XREAL_1:6; then A33: ((Gauge (C,m)) * (i1,j1)) `1 <= p `1 by A11, XXREAL_0:2; ((Gauge (C,m)) * (i1,j1)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * ((j1 - 2) / 1)) by A32, EUCLID:52 .= (S-bound C) + ((((N-bound C) - (S-bound C)) / 1) * ((j1 - 2) / (2 |^ m))) by XCMPLX_1:85 ; then ((Gauge (C,m)) * (i1,j1)) `2 <= ((Gauge (C,n)) * (i,j)) `2 by A12, A24, XREAL_1:6; then A34: ((Gauge (C,m)) * (i1,j1)) `2 <= p `2 by A17, XXREAL_0:2; ( 1 <= i1 + 1 & j1 <= width (Gauge (C,m)) ) by A28, NAT_1:11, NAT_1:13; then [(i1 + 1),j1] in Indices (Gauge (C,m)) by A26, A30, MATRIX_1:36; then (Gauge (C,m)) * ((i1 + 1),j1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * ((i1 + 1) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ m)) * (j1 - 2)))]| by JORDAN8:def_1; then ((Gauge (C,m)) * ((i1 + 1),j1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ m)) * (((i1 + 1) - 2) / 1)) by EUCLID:52 .= (W-bound C) + ((((E-bound C) - (W-bound C)) / 1) * (((i1 + 1) - 2) / (2 |^ m))) by XCMPLX_1:85 ; then ((Gauge (C,n)) * ((i + 1),j)) `1 <= ((Gauge (C,m)) * ((i1 + 1),j1)) `1 by A18, A22, XREAL_1:6; then p `1 <= ((Gauge (C,m)) * ((i1 + 1),j1)) `1 by A13, XXREAL_0:2; hence e in cell ((Gauge (C,m)),i1,j1) by A20, A26, A30, A28, A33, A34, A31, JORDAN9:17; ::_thesis: verum end; theorem Th38: :: JORDAN1H:38 for m, n, i, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds ex i1, j1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) proof let m, n, i, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds ex i1, j1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) implies ex i1, j1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) ) assume that A1: m <= n and A2: ( 1 <= i & i + 1 <= len (Gauge (C,n)) ) and A3: ( 1 <= j & j + 1 <= width (Gauge (C,n)) ) ; ::_thesis: ex i1, j1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) consider i1, j1 being Element of NAT such that A4: i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] and A5: j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] and A6: cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) by A1, A2, A3, Th37; take i1 ; ::_thesis: ex j1 being Element of NAT st ( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) take j1 ; ::_thesis: ( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) thus ( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) ) by A1, A2, A4, Th36; ::_thesis: ( 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) ) ( len (Gauge (C,m)) = width (Gauge (C,m)) & len (Gauge (C,n)) = width (Gauge (C,n)) ) by JORDAN8:def_1; hence ( 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) ) by A1, A3, A5, Th36; ::_thesis: cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) thus cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) by A6; ::_thesis: verum end; theorem :: JORDAN1H:39 for P being Subset of (TOP-REAL 2) st P is bounded holds not UBD P is bounded proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is bounded implies not UBD P is bounded ) assume P is bounded ; ::_thesis: not UBD P is bounded then UBD P is_outside_component_of P by JORDAN2C:68; hence not UBD P is bounded by JORDAN2C:def_3; ::_thesis: verum end; theorem Th40: :: JORDAN1H:40 for p being Point of (TOP-REAL 2) for f being non constant standard special_circular_sequence st Rotate (f,p) is clockwise_oriented holds f is clockwise_oriented proof let p be Point of (TOP-REAL 2); ::_thesis: for f being non constant standard special_circular_sequence st Rotate (f,p) is clockwise_oriented holds f is clockwise_oriented let f be non constant standard special_circular_sequence; ::_thesis: ( Rotate (f,p) is clockwise_oriented implies f is clockwise_oriented ) assume Rotate (f,p) is clockwise_oriented ; ::_thesis: f is clockwise_oriented then reconsider g = Rotate (f,p) as non constant standard clockwise_oriented special_circular_sequence ; for i being Element of NAT st 1 < i & i < len f holds f /. i <> f /. 1 by GOBOARD7:36; then f = Rotate (g,(f /. 1)) by REVROT_1:16; hence f is clockwise_oriented ; ::_thesis: verum end; theorem :: JORDAN1H:41 for f being non constant standard special_circular_sequence st LeftComp f = UBD (L~ f) holds f is clockwise_oriented proof let f be non constant standard special_circular_sequence; ::_thesis: ( LeftComp f = UBD (L~ f) implies f is clockwise_oriented ) assume A1: LeftComp f = UBD (L~ f) ; ::_thesis: f is clockwise_oriented set g = Rotate (f,(N-min (L~ f))); assume not f is clockwise_oriented ; ::_thesis: contradiction then not Rotate (f,(N-min (L~ f))) is clockwise_oriented by Th40; then A2: Rev (Rotate (f,(N-min (L~ f)))) is clockwise_oriented by REVROT_1:38; L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33; then UBD (L~ f) = UBD (L~ (Rev (Rotate (f,(N-min (L~ f)))))) by SPPOL_2:22 .= LeftComp (Rev (Rotate (f,(N-min (L~ f))))) by A2, GOBRD14:36 .= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD9:23 .= RightComp f by REVROT_1:37 ; hence contradiction by A1, SPRECT_4:6; ::_thesis: verum end; begin theorem Th42: :: JORDAN1H:42 for f being non constant standard special_circular_sequence holds (Cl (LeftComp f)) ` = RightComp f proof let f be non constant standard special_circular_sequence; ::_thesis: (Cl (LeftComp f)) ` = RightComp f A1: (Cl (LeftComp f)) ` misses Cl (LeftComp f) by SUBSET_1:24; (Cl (LeftComp f)) \/ (RightComp f) = ((L~ f) \/ (LeftComp f)) \/ (RightComp f) by GOBRD14:22 .= ((L~ f) \/ (RightComp f)) \/ (LeftComp f) by XBOOLE_1:4 .= the carrier of (TOP-REAL 2) by GOBRD14:15 ; hence (Cl (LeftComp f)) ` c= RightComp f by A1, XBOOLE_1:73; :: according to XBOOLE_0:def_10 ::_thesis: RightComp f c= (Cl (LeftComp f)) ` A2: RightComp f misses LeftComp f by GOBRD14:14; ( Cl (LeftComp f) = (LeftComp f) \/ (L~ f) & L~ f misses RightComp f ) by GOBRD14:22, SPRECT_3:25; then Cl (LeftComp f) misses RightComp f by A2, XBOOLE_1:70; hence RightComp f c= (Cl (LeftComp f)) ` by SUBSET_1:23; ::_thesis: verum end; theorem :: JORDAN1H:43 for f being non constant standard special_circular_sequence holds (Cl (RightComp f)) ` = LeftComp f proof let f be non constant standard special_circular_sequence; ::_thesis: (Cl (RightComp f)) ` = LeftComp f A1: (Cl (RightComp f)) ` misses Cl (RightComp f) by SUBSET_1:24; (Cl (RightComp f)) \/ (LeftComp f) = ((L~ f) \/ (RightComp f)) \/ (LeftComp f) by GOBRD14:21 .= the carrier of (TOP-REAL 2) by GOBRD14:15 ; hence (Cl (RightComp f)) ` c= LeftComp f by A1, XBOOLE_1:73; :: according to XBOOLE_0:def_10 ::_thesis: LeftComp f c= (Cl (RightComp f)) ` A2: LeftComp f misses RightComp f by GOBRD14:14; ( Cl (RightComp f) = (RightComp f) \/ (L~ f) & L~ f misses LeftComp f ) by GOBRD14:21, SPRECT_3:26; then Cl (RightComp f) misses LeftComp f by A2, XBOOLE_1:70; hence LeftComp f c= (Cl (RightComp f)) ` by SUBSET_1:23; ::_thesis: verum end; theorem Th44: :: JORDAN1H:44 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds GoB (Cage (C,n)) = Gauge (C,n) proof let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds GoB (Cage (C,n)) = Gauge (C,n) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( C is connected implies GoB (Cage (C,n)) = Gauge (C,n) ) A1: ( S-max (L~ (Cage (C,n))) in rng (Cage (C,n)) & E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) ) by SPRECT_2:42, SPRECT_2:46; assume A2: C is connected ; ::_thesis: GoB (Cage (C,n)) = Gauge (C,n) then consider iw being Element of NAT such that A3: ( 1 <= iw & iw <= width (Gauge (C,n)) ) and A4: W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,iw) by JORDAN1D:30; A5: ( N-min (L~ (Cage (C,n))) in rng (Cage (C,n)) & Cage (C,n) is_sequence_on Gauge (C,n) ) by A2, JORDAN9:def_1, SPRECT_2:39; consider ie being Element of NAT such that A6: ( 1 <= ie & ie <= width (Gauge (C,n)) ) and A7: (Gauge (C,n)) * ((len (Gauge (C,n))),ie) = E-max (L~ (Cage (C,n))) by A2, JORDAN1D:25; A8: 1 <= len (Gauge (C,n)) by GOBRD11:34; then A9: [(len (Gauge (C,n))),ie] in Indices (Gauge (C,n)) by A6, MATRIX_1:36; consider iS being Element of NAT such that A10: ( 1 <= iS & iS <= len (Gauge (C,n)) ) and A11: (Gauge (C,n)) * (iS,1) = S-max (L~ (Cage (C,n))) by A2, JORDAN1D:28; A12: 1 <= width (Gauge (C,n)) by GOBRD11:34; then A13: [iS,1] in Indices (Gauge (C,n)) by A10, MATRIX_1:36; consider IN being Element of NAT such that A14: ( 1 <= IN & IN <= len (Gauge (C,n)) ) and A15: (Gauge (C,n)) * (IN,(width (Gauge (C,n)))) = N-min (L~ (Cage (C,n))) by A2, JORDAN1D:21; A16: [IN,(width (Gauge (C,n)))] in Indices (Gauge (C,n)) by A12, A14, MATRIX_1:36; [1,iw] in Indices (Gauge (C,n)) by A8, A3, MATRIX_1:36; hence GoB (Cage (C,n)) = Gauge (C,n) by A4, A11, A13, A7, A9, A1, A15, A16, A5, Th34, SPRECT_2:43; ::_thesis: verum end; theorem :: JORDAN1H:45 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds N-min C in right_cell ((Cage (C,n)),1) proof let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds N-min C in right_cell ((Cage (C,n)),1) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( C is connected implies N-min C in right_cell ((Cage (C,n)),1) ) assume A1: C is connected ; ::_thesis: N-min C in right_cell ((Cage (C,n)),1) then consider i being Element of NAT such that A2: 1 <= i and A3: i + 1 <= len (Gauge (C,n)) and A4: (Cage (C,n)) /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) and A5: (Cage (C,n)) /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) and A6: N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) and N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) by JORDAN9:def_1; A7: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB (Cage (C,n))) & [i2,j2] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. 1 = (GoB (Cage (C,n))) * (i1,j1) & (Cage (C,n)) /. (1 + 1) = (GoB (Cage (C,n))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2) ) holds ( i1 = i2 & j1 = j2 + 1 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2) ) proof 0 <> width (Gauge (C,n)) by GOBOARD1:def_3; then A8: 1 <= width (Gauge (C,n)) by NAT_1:14; A9: GoB (Cage (C,n)) = Gauge (C,n) by A1, Th44; let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB (Cage (C,n))) & [i2,j2] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. 1 = (GoB (Cage (C,n))) * (i1,j1) & (Cage (C,n)) /. (1 + 1) = (GoB (Cage (C,n))) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2) ) implies ( i1 = i2 & j1 = j2 + 1 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2) ) ) assume that A10: [i1,j1] in Indices (GoB (Cage (C,n))) and A11: [i2,j2] in Indices (GoB (Cage (C,n))) and A12: (Cage (C,n)) /. 1 = (GoB (Cage (C,n))) * (i1,j1) and A13: (Cage (C,n)) /. (1 + 1) = (GoB (Cage (C,n))) * (i2,j2) ; ::_thesis: ( ( i1 = i2 & j1 + 1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1) ) or ( i1 + 1 = i2 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2) ) or ( i1 = i2 & j1 = j2 + 1 & cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2) ) ) 1 <= i + 1 by NAT_1:11; then A14: [(i + 1),(width (Gauge (C,n)))] in Indices (Gauge (C,n)) by A3, A8, MATRIX_1:36; then A15: i2 = i + 1 by A5, A11, A13, A9, GOBOARD1:5; i < len (Gauge (C,n)) by A3, NAT_1:13; then A16: [i,(width (Gauge (C,n)))] in Indices (Gauge (C,n)) by A2, A8, MATRIX_1:36; then A17: i1 = i by A4, A10, A12, A9, GOBOARD1:5; A18: j2 = width (Gauge (C,n)) by A5, A11, A13, A9, A14, GOBOARD1:5; 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 A4, A10, A12, A9, A16, A15, A18, GOBOARD1:5; case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1) hence cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,j1) by A17, A15; ::_thesis: verum end; case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1)) thus cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i1,(j1 -' 1)) by A4, A10, A12, A9, A16, A17, GOBOARD1:5; ::_thesis: verum end; case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2) hence cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),i2,j2) by A17, A15; ::_thesis: verum end; case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2) hence cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) = cell ((GoB (Cage (C,n))),(i1 -' 1),j2) by A17, A15; ::_thesis: verum end; end; end; 1 + 1 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2; hence N-min C in right_cell ((Cage (C,n)),1) by A6, A7, GOBOARD5:def_6; ::_thesis: verum end; theorem Th46: :: JORDAN1H:46 for i, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i))) proof let i, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i))) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( C is connected & i <= j implies L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i))) ) assume that A1: C is connected and A2: i <= j and A3: not L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i))) ; ::_thesis: contradiction A4: Cage (C,j) is_sequence_on Gauge (C,j) by A1, JORDAN9:def_1; A5: GoB (Cage (C,i)) = Gauge (C,i) by A1, Th44; consider p being Point of (TOP-REAL 2) such that A6: p in L~ (Cage (C,j)) and A7: not p in Cl (RightComp (Cage (C,i))) by A3, SUBSET_1:2; consider i1 being Element of NAT such that A8: 1 <= i1 and A9: i1 + 1 <= len (Cage (C,j)) and A10: p in LSeg ((Cage (C,j)),i1) by A6, SPPOL_2:13; A11: GoB (Cage (C,j)) = Gauge (C,j) by A1, Th44; then A12: right_cell ((Cage (C,j)),i1,(Gauge (C,j))) = right_cell ((Cage (C,j)),i1) by A8, A9, Th23; A13: i1 < len (Cage (C,j)) by A9, NAT_1:13; now__::_thesis:_right_cell_((Cage_(C,j)),i1)_c=_Cl_(LeftComp_(Cage_(C,i))) ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) proof set f = Cage (C,j); A14: i1 in dom (Cage (C,j)) by A8, A13, FINSEQ_3:25; then consider i4, j4 being Element of NAT such that A15: [i4,j4] in Indices (Gauge (C,j)) and A16: (Cage (C,j)) /. i1 = (Gauge (C,j)) * (i4,j4) by A4, GOBOARD1:def_9; A17: 1 <= i4 by A15, MATRIX_1:38; A18: j4 <= width (Gauge (C,j)) by A15, MATRIX_1:38; A19: 1 <= j4 by A15, MATRIX_1:38; A20: i4 <= len (Gauge (C,j)) by A15, MATRIX_1:38; 1 <= i1 + 1 by NAT_1:11; then A21: i1 + 1 in dom (Cage (C,j)) by A9, FINSEQ_3:25; then consider i5, j5 being Element of NAT such that A22: [i5,j5] in Indices (Gauge (C,j)) and A23: (Cage (C,j)) /. (i1 + 1) = (Gauge (C,j)) * (i5,j5) by A4, GOBOARD1:def_9; A24: 1 <= i5 by A22, MATRIX_1:38; right_cell ((Cage (C,j)),i1) = right_cell ((Cage (C,j)),i1) ; then A25: ( ( i4 = i5 & j4 + 1 = j5 & right_cell ((Cage (C,j)),i1) = cell ((GoB (Cage (C,j))),i4,j4) ) or ( i4 + 1 = i5 & j4 = j5 & right_cell ((Cage (C,j)),i1) = cell ((GoB (Cage (C,j))),i4,(j4 -' 1)) ) or ( i4 = i5 + 1 & j4 = j5 & right_cell ((Cage (C,j)),i1) = cell ((GoB (Cage (C,j))),i5,j5) ) or ( i4 = i5 & j4 = j5 + 1 & right_cell ((Cage (C,j)),i1) = cell ((GoB (Cage (C,j))),(i4 -' 1),j5) ) ) by A8, A9, A11, A15, A16, A22, A23, GOBOARD5:def_6; (abs (i4 - i5)) + (abs (j4 - j5)) = 1 by A4, A14, A15, A16, A21, A22, A23, GOBOARD1:def_9; then A26: ( ( abs (i4 - i5) = 1 & j4 = j5 ) or ( abs (j4 - j5) = 1 & i4 = i5 ) ) by SEQM_3:42; A27: j5 <= width (Gauge (C,j)) by A22, MATRIX_1:38; A28: i5 <= len (Gauge (C,j)) by A22, MATRIX_1:38; A29: 1 <= j5 by A22, MATRIX_1:38; percases ( ( i4 = i5 & j4 + 1 = j5 ) or ( i4 + 1 = i5 & j4 = j5 ) or ( i4 = i5 + 1 & j4 = j5 ) or ( i4 = i5 & j4 = j5 + 1 ) ) by A26, SEQM_3:41; supposeA30: ( i4 = i5 & j4 + 1 = j5 ) ; ::_thesis: ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) then i4 < len (Gauge (C,j)) by A1, A8, A9, A15, A16, A22, A23, JORDAN10:1; then i4 + 1 <= len (Gauge (C,j)) by NAT_1:13; hence ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A11, A17, A19, A27, A25, A30, Th38; ::_thesis: verum end; supposeA31: ( i4 + 1 = i5 & j4 = j5 ) ; ::_thesis: ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) then 1 < j4 by A1, A8, A9, A15, A16, A22, A23, JORDAN10:3; then 1 + 1 <= j4 by NAT_1:13; then A32: 1 <= j4 -' 1 by JORDAN5B:2; (j4 -' 1) + 1 = j4 by A19, XREAL_1:235; hence ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A11, A17, A18, A28, A25, A31, A32, Th38; ::_thesis: verum end; supposeA33: ( i4 = i5 + 1 & j4 = j5 ) ; ::_thesis: ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) then j5 < width (Gauge (C,j)) by A1, A8, A9, A15, A16, A22, A23, JORDAN10:4; then j5 + 1 <= width (Gauge (C,j)) by NAT_1:13; hence ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A11, A20, A24, A29, A25, A33, Th38; ::_thesis: verum end; supposeA34: ( i4 = i5 & j4 = j5 + 1 ) ; ::_thesis: ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) then 1 < i4 by A1, A8, A9, A15, A16, A22, A23, JORDAN10:2; then 1 + 1 <= i4 by NAT_1:13; then A35: 1 <= i4 -' 1 by JORDAN5B:2; (i4 -' 1) + 1 = i4 by A17, XREAL_1:235; hence ex i2, j2 being Element of NAT st ( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A11, A20, A18, A29, A25, A34, A35, Th38; ::_thesis: verum end; end; end; then consider i2, j2 being Element of NAT such that 1 <= i2 and A36: i2 + 1 <= len (Gauge (C,i)) and 1 <= j2 and A37: j2 + 1 <= width (Gauge (C,i)) and A38: right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ; A39: Int (right_cell ((Cage (C,j)),i1)) c= Int (cell ((Gauge (C,i)),i2,j2)) by A38, TOPS_1:19; A40: RightComp (Cage (C,i)) is_a_component_of (L~ (Cage (C,i))) ` by GOBOARD9:def_2; A41: (Cl (LeftComp (Cage (C,i)))) \/ (RightComp (Cage (C,i))) = ((L~ (Cage (C,i))) \/ (LeftComp (Cage (C,i)))) \/ (RightComp (Cage (C,i))) by GOBRD14:22 .= ((L~ (Cage (C,i))) \/ (RightComp (Cage (C,i)))) \/ (LeftComp (Cage (C,i))) by XBOOLE_1:4 .= the carrier of (TOP-REAL 2) by GOBRD14:15 ; assume not right_cell ((Cage (C,j)),i1) c= Cl (LeftComp (Cage (C,i))) ; ::_thesis: contradiction then not cell ((Gauge (C,i)),i2,j2) c= Cl (LeftComp (Cage (C,i))) by A38, XBOOLE_1:1; then A42: cell ((Gauge (C,i)),i2,j2) meets RightComp (Cage (C,i)) by A41, XBOOLE_1:73; A43: ( i2 < len (Gauge (C,i)) & j2 < width (Gauge (C,i)) ) by A36, A37, NAT_1:13; then cell ((Gauge (C,i)),i2,j2) = Cl (Int (cell ((Gauge (C,i)),i2,j2))) by GOBRD11:35; then A44: Int (cell ((Gauge (C,i)),i2,j2)) meets RightComp (Cage (C,i)) by A42, TSEP_1:36; A45: Int (cell ((Gauge (C,i)),i2,j2)) is convex by A43, GOBOARD9:17; Int (cell ((Gauge (C,i)),i2,j2)) c= (L~ (Cage (C,i))) ` by A5, A43, GOBRD12:1; then Int (cell ((Gauge (C,i)),i2,j2)) c= RightComp (Cage (C,i)) by A44, A40, A45, GOBOARD9:4; then Int (right_cell ((Cage (C,j)),i1)) c= RightComp (Cage (C,i)) by A39, XBOOLE_1:1; then Cl (Int (right_cell ((Cage (C,j)),i1))) c= Cl (RightComp (Cage (C,i))) by PRE_TOPC:19; then A46: right_cell ((Cage (C,j)),i1) c= Cl (RightComp (Cage (C,i))) by A4, A8, A9, A12, JORDAN9:11; ( LSeg ((Cage (C,j)),i1) c= right_cell ((Cage (C,j)),i1,(Gauge (C,j))) & right_cell ((Cage (C,j)),i1,(Gauge (C,j))) c= right_cell ((Cage (C,j)),i1) ) by A4, A8, A9, Th22, GOBRD13:33; then LSeg ((Cage (C,j)),i1) c= right_cell ((Cage (C,j)),i1) by XBOOLE_1:1; then LSeg ((Cage (C,j)),i1) c= Cl (RightComp (Cage (C,i))) by A46, XBOOLE_1:1; hence contradiction by A7, A10; ::_thesis: verum end; then A47: C meets Cl (LeftComp (Cage (C,i))) by A1, A8, A9, A12, JORDAN9:31, XBOOLE_1:63; ( Cl (LeftComp (Cage (C,i))) = (LeftComp (Cage (C,i))) \/ (L~ (Cage (C,i))) & C misses L~ (Cage (C,i)) ) by A1, GOBRD14:22, JORDAN10:5; then A48: C meets LeftComp (Cage (C,i)) by A47, XBOOLE_1:70; reconsider D = (L~ (Cage (C,i))) ` as Subset of (TOP-REAL 2) ; D = (LeftComp (Cage (C,i))) \/ (RightComp (Cage (C,i))) by GOBRD12:10; then A49: RightComp (Cage (C,i)) c= D by XBOOLE_1:7; C c= RightComp (Cage (C,i)) by A1, JORDAN10:11; then A50: C c= D by A49, XBOOLE_1:1; C meets C ; then A51: C meets RightComp (Cage (C,i)) by A1, JORDAN10:11, XBOOLE_1:63; ( LeftComp (Cage (C,i)) is_a_component_of D & RightComp (Cage (C,i)) is_a_component_of D ) by GOBOARD9:def_1, GOBOARD9:def_2; hence contradiction by A1, A48, A50, A51, JORDAN9:1, SPRECT_4:6; ::_thesis: verum end; theorem Th47: :: JORDAN1H:47 for i, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) proof let i, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( C is connected & i <= j implies LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) ) assume that A1: C is connected and A2: i <= j ; ::_thesis: LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) A3: (Cage (C,j)) /. 1 = N-min (L~ (Cage (C,j))) by A1, JORDAN9:32; ( i < j or i = j ) by A2, XXREAL_0:1; then A4: ( E-bound (L~ (Cage (C,i))) > E-bound (L~ (Cage (C,j))) or E-bound (L~ (Cage (C,i))) = E-bound (L~ (Cage (C,j))) ) by A1, JORDAN1A:67; set p = |[((E-bound (L~ (Cage (C,i)))) + 1),0]|; A5: LeftComp (Cage (C,i)) misses RightComp (Cage (C,i)) by GOBRD14:14; A6: |[((E-bound (L~ (Cage (C,i)))) + 1),0]| `1 = (E-bound (L~ (Cage (C,i)))) + 1 by EUCLID:52; then |[((E-bound (L~ (Cage (C,i)))) + 1),0]| `1 > E-bound (L~ (Cage (C,i))) by XREAL_1:29; then |[((E-bound (L~ (Cage (C,i)))) + 1),0]| `1 > E-bound (L~ (Cage (C,j))) by A4, XXREAL_0:2; then A7: |[((E-bound (L~ (Cage (C,i)))) + 1),0]| in LeftComp (Cage (C,j)) by A3, JORDAN2C:111; (Cage (C,i)) /. 1 = N-min (L~ (Cage (C,i))) by A1, JORDAN9:32; then |[((E-bound (L~ (Cage (C,i)))) + 1),0]| in LeftComp (Cage (C,i)) by A6, JORDAN2C:111, XREAL_1:29; then A8: LeftComp (Cage (C,i)) meets LeftComp (Cage (C,j)) by A7, XBOOLE_0:3; ( Cl (RightComp (Cage (C,i))) = (RightComp (Cage (C,i))) \/ (L~ (Cage (C,i))) & L~ (Cage (C,i)) misses LeftComp (Cage (C,i)) ) by GOBRD14:21, SPRECT_3:26; then Cl (RightComp (Cage (C,i))) misses LeftComp (Cage (C,i)) by A5, XBOOLE_1:70; then L~ (Cage (C,j)) misses LeftComp (Cage (C,i)) by A1, A2, Th46, XBOOLE_1:63; then ( LeftComp (Cage (C,j)) is_a_component_of (L~ (Cage (C,j))) ` & LeftComp (Cage (C,i)) c= (L~ (Cage (C,j))) ` ) by GOBOARD9:def_1, SUBSET_1:23; hence LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) by A8, GOBOARD9:4; ::_thesis: verum end; theorem :: JORDAN1H:48 for i, j being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds RightComp (Cage (C,j)) c= RightComp (Cage (C,i)) proof let i, j be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds RightComp (Cage (C,j)) c= RightComp (Cage (C,i)) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( C is connected & i <= j implies RightComp (Cage (C,j)) c= RightComp (Cage (C,i)) ) assume ( C is connected & i <= j ) ; ::_thesis: RightComp (Cage (C,j)) c= RightComp (Cage (C,i)) then A1: Cl (LeftComp (Cage (C,i))) c= Cl (LeftComp (Cage (C,j))) by Th47, PRE_TOPC:19; ( (Cl (LeftComp (Cage (C,i)))) ` = RightComp (Cage (C,i)) & (Cl (LeftComp (Cage (C,j)))) ` = RightComp (Cage (C,j)) ) by Th42; hence RightComp (Cage (C,j)) c= RightComp (Cage (C,i)) by A1, SUBSET_1:12; ::_thesis: verum end; begin definition let C be compact non horizontal non vertical Subset of (TOP-REAL 2); let n be Element of NAT ; func X-SpanStart (C,n) -> Element of NAT equals :: JORDAN1H:def 2 (2 |^ (n -' 1)) + 2; correctness coherence (2 |^ (n -' 1)) + 2 is Element of NAT ; ; end; :: deftheorem defines X-SpanStart JORDAN1H:def_2_:_ for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT holds X-SpanStart (C,n) = (2 |^ (n -' 1)) + 2; theorem Th49: :: JORDAN1H:49 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( 2 < X-SpanStart (C,n) & X-SpanStart (C,n) < len (Gauge (C,n)) ) proof let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( 2 < X-SpanStart (C,n) & X-SpanStart (C,n) < len (Gauge (C,n)) ) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 2 < X-SpanStart (C,n) & X-SpanStart (C,n) < len (Gauge (C,n)) ) 2 |^ (n -' 1) > 0 by NEWTON:83; then (2 |^ (n -' 1)) + 2 > 0 + 2 by XREAL_1:6; hence 2 < X-SpanStart (C,n) ; ::_thesis: X-SpanStart (C,n) < len (Gauge (C,n)) n -' 1 <= n by NAT_D:44; then ( len (Gauge (C,n)) = (2 |^ n) + 3 & 2 |^ (n -' 1) <= 2 |^ n ) by JORDAN8:def_1, PREPOWER:93; hence X-SpanStart (C,n) < len (Gauge (C,n)) by XREAL_1:8; ::_thesis: verum end; theorem Th50: :: JORDAN1H:50 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( 1 <= (X-SpanStart (C,n)) -' 1 & (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) ) proof let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds ( 1 <= (X-SpanStart (C,n)) -' 1 & (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) ) let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 1 <= (X-SpanStart (C,n)) -' 1 & (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) ) 2 < X-SpanStart (C,n) by Th49; then A1: ((X-SpanStart (C,n)) -' 1) + 1 = X-SpanStart (C,n) by XREAL_1:235, XXREAL_0:2; 1 < X-SpanStart (C,n) by Th49, XXREAL_0:2; hence 1 <= (X-SpanStart (C,n)) -' 1 by A1, NAT_1:13; ::_thesis: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) ( X-SpanStart (C,n) < len (Gauge (C,n)) & (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) ) by Th49, NAT_D:44; hence (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by XXREAL_0:2; ::_thesis: verum end; definition let C be compact non horizontal non vertical Subset of (TOP-REAL 2); let n be Element of NAT ; predn is_sufficiently_large_for C means :Def3: :: JORDAN1H:def 3 ex j being Element of NAT st ( j < width (Gauge (C,n)) & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C ); end; :: deftheorem Def3 defines is_sufficiently_large_for JORDAN1H:def_3_:_ for C being compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT holds ( n is_sufficiently_large_for C iff ex j being Element of NAT st ( j < width (Gauge (C,n)) & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C ) ); theorem :: JORDAN1H:51 for n being Element of NAT for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds n >= 1 proof let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds n >= 1 let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( n is_sufficiently_large_for C implies n >= 1 ) A1: 2 |^ 0 = 1 by NEWTON:4; assume n is_sufficiently_large_for C ; ::_thesis: n >= 1 then consider j being Element of NAT such that A2: j < width (Gauge (C,n)) and A3: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C by Def3; assume n < 1 ; ::_thesis: contradiction then A4: n = 0 by NAT_1:14; A5: j > 1 proof A6: (X-SpanStart (C,n)) -' 1 <= len (Gauge (C,n)) by Th50; assume A7: j <= 1 ; ::_thesis: contradiction percases ( j = 0 or j = 1 ) by A7, NAT_1:25; supposeA8: j = 0 ; ::_thesis: contradiction 0 <= width (Gauge (C,n)) ; then A9: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) is empty by A6, JORDAN1A:24; cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A6, JORDAN1A:49; hence contradiction by A3, A8, A9, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum end; supposeA10: j = 1 ; ::_thesis: contradiction set i1 = X-SpanStart (C,n); UBD C is_outside_component_of C by JORDAN2C:68; then A11: UBD C is_a_component_of C ` by JORDAN2C:def_3; ( X-SpanStart (C,n) < len (Gauge (C,n)) & (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) ) by Th49, NAT_D:44; then A12: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by XXREAL_0:2; BDD C c= C ` by JORDAN2C:25; then A13: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= C ` by A3, A10, XBOOLE_1:1; A14: width (Gauge (C,n)) <> 0 by GOBOARD1:def_3; then A15: 0 + 1 <= width (Gauge (C,n)) by NAT_1:14; then A16: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) is empty by A6, JORDAN1A:24; 1 <= (X-SpanStart (C,n)) -' 1 by Th50; then (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0)) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1))) = LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(0 + 1))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(0 + 1)))) by A14, A12, GOBOARD5:26; then A17: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) meets cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1)) by XBOOLE_0:def_7; cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0) c= UBD C by A6, JORDAN1A:49; then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),1) c= UBD C by A15, A12, A17, A11, A13, GOBOARD9:4, JORDAN1A:25; hence contradiction by A3, A10, A16, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum end; end; end; A18: width (Gauge (C,n)) = (2 |^ n) + 3 by JORDAN1A:28; then A19: j <= 3 + 1 by A2, A4, NEWTON:4; A20: j + 1 < width (Gauge (C,n)) proof assume j + 1 >= width (Gauge (C,n)) ; ::_thesis: contradiction then A21: ( j + 1 > width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) ) by XXREAL_0:1; A22: (X-SpanStart (C,n)) -' 1 <= len (Gauge (C,n)) by Th50; percases ( j = width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) ) by A2, A21, NAT_1:13; supposeA23: j = width (Gauge (C,n)) ; ::_thesis: contradiction ( not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) is empty & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) c= UBD C ) by A22, JORDAN1A:24, JORDAN1A:50; hence contradiction by A3, A23, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum end; suppose j + 1 = width (Gauge (C,n)) ; ::_thesis: contradiction then A24: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= BDD C by A3, NAT_D:34; BDD C c= C ` by JORDAN2C:25; then A25: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= C ` by A24, XBOOLE_1:1; set i1 = X-SpanStart (C,n); A26: (width (Gauge (C,n))) - 1 < width (Gauge (C,n)) by XREAL_1:146; UBD C is_outside_component_of C by JORDAN2C:68; then A27: UBD C is_a_component_of C ` by JORDAN2C:def_3; (width (Gauge (C,n))) -' 1 <= width (Gauge (C,n)) by NAT_D:44; then A28: not cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) is empty by A22, JORDAN1A:24; A29: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) c= UBD C by A22, JORDAN1A:50; A30: 1 <= (X-SpanStart (C,n)) -' 1 by Th50; ( X-SpanStart (C,n) < len (Gauge (C,n)) & (X-SpanStart (C,n)) -' 1 <= X-SpanStart (C,n) ) by Th49, NAT_D:44; then A31: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by XXREAL_0:2; A32: width (Gauge (C,n)) <> 0 by GOBOARD1:def_3; then ((width (Gauge (C,n))) -' 1) + 1 = width (Gauge (C,n)) by NAT_1:14, XREAL_1:235; then (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n))))) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1))) = LSeg (((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n))))),((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(width (Gauge (C,n)))))) by A31, A26, A30, GOBOARD5:26; then A33: cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n)))) meets cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) by XBOOLE_0:def_7; (width (Gauge (C,n))) -' 1 < width (Gauge (C,n)) by A32, A26, NAT_1:14, XREAL_1:233; then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1)) c= UBD C by A29, A31, A33, A27, A25, GOBOARD9:4, JORDAN1A:25; hence contradiction by A24, A28, JORDAN2C:24, XBOOLE_1:68; ::_thesis: verum end; end; end; percases ( j = 0 or j = 1 or j = 2 or j = 3 or j = 4 ) by A19, NAT_1:28; suppose ( j = 0 or j = 1 ) ; ::_thesis: contradiction hence contradiction by A5; ::_thesis: verum end; supposeA34: j = 2 ; ::_thesis: contradiction A35: X-SpanStart (C,0) = 1 + 2 by A1, NAT_2:8; then (X-SpanStart (C,0)) -' 1 = (X-SpanStart (C,0)) - 1 by NAT_D:39 .= 2 by A35 ; hence contradiction by A3, A4, A34, JORDAN1B:18; ::_thesis: verum end; suppose ( j = 3 or j = 4 ) ; ::_thesis: contradiction hence contradiction by A18, A20, A1, A4; ::_thesis: verum end; end; end; theorem :: JORDAN1H:52 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) proof let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) set G = Gauge (C,n); let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) ) assume that A1: f is_sequence_on Gauge (C,n) and A2: len f > 1 ; ::_thesis: for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235; let i1, j1 be Element of NAT ; ::_thesis: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) implies [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) ) assume that A4: left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C and A5: [i1,j1] in Indices (Gauge (C,n)) and A6: f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) and A7: [i1,(j1 + 1)] in Indices (Gauge (C,n)) and A8: f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) ; ::_thesis: [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) A9: 1 <= i1 by A7, MATRIX_1:38; A10: ( len (Gauge (C,n)) = width (Gauge (C,n)) & j1 <= width (Gauge (C,n)) ) by A5, JORDAN8:def_1, MATRIX_1:38; A11: now__::_thesis:_not_i1_-'_1_<_1 assume i1 -' 1 < 1 ; ::_thesis: contradiction then i1 <= 1 by NAT_1:14, NAT_D:36; then i1 = 1 by A9, XXREAL_0:1; then cell ((Gauge (C,n)),(1 -' 1),j1) meets C by A1, A4, A5, A6, A7, A8, A3, GOBRD13:21; then cell ((Gauge (C,n)),0,j1) meets C by XREAL_1:232; hence contradiction by A10, JORDAN8:18; ::_thesis: verum end; A12: i1 -' 1 <= i1 by NAT_D:35; i1 <= len (Gauge (C,n)) by A5, MATRIX_1:38; then A13: i1 -' 1 <= len (Gauge (C,n)) by A12, XXREAL_0:2; ( 1 <= j1 + 1 & j1 + 1 <= width (Gauge (C,n)) ) by A7, MATRIX_1:38; hence [(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n)) by A13, A11, MATRIX_1:36; ::_thesis: verum end; theorem :: JORDAN1H:53 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) proof let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) set G = Gauge (C,n); let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) ) assume that A1: f is_sequence_on Gauge (C,n) and A2: len f > 1 ; ::_thesis: for i1, j1 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235; A4: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; let i1, j1 be Element of NAT ; ::_thesis: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) implies [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) ) assume that A5: left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C and A6: [i1,j1] in Indices (Gauge (C,n)) and A7: f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) and A8: [(i1 + 1),j1] in Indices (Gauge (C,n)) and A9: f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) ; ::_thesis: [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) A10: j1 <= width (Gauge (C,n)) by A8, MATRIX_1:38; A11: i1 <= len (Gauge (C,n)) by A6, MATRIX_1:38; A12: now__::_thesis:_not_j1_+_1_>_len_(Gauge_(C,n)) assume j1 + 1 > len (Gauge (C,n)) ; ::_thesis: contradiction then A13: (len (Gauge (C,n))) + 1 <= j1 + 1 by NAT_1:13; j1 + 1 <= (len (Gauge (C,n))) + 1 by A4, A10, XREAL_1:6; then j1 + 1 = (len (Gauge (C,n))) + 1 by A13, XXREAL_0:1; then cell ((Gauge (C,n)),i1,(len (Gauge (C,n)))) meets C by A1, A5, A6, A7, A8, A9, A3, GOBRD13:23; hence contradiction by A11, JORDAN8:15; ::_thesis: verum end; A14: 1 <= j1 + 1 by NAT_1:11; ( 1 <= i1 + 1 & i1 + 1 <= len (Gauge (C,n)) ) by A8, MATRIX_1:38; hence [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) by A4, A14, A12, MATRIX_1:36; ::_thesis: verum end; theorem :: JORDAN1H:54 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for j1, i2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [i2,(j1 -' 1)] in Indices (Gauge (C,n)) proof let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for j1, i2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [i2,(j1 -' 1)] in Indices (Gauge (C,n)) let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for j1, i2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [i2,(j1 -' 1)] in Indices (Gauge (C,n)) set G = Gauge (C,n); let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for j1, i2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [i2,(j1 -' 1)] in Indices (Gauge (C,n)) ) assume that A1: f is_sequence_on Gauge (C,n) and A2: len f > 1 ; ::_thesis: for j1, i2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [i2,(j1 -' 1)] in Indices (Gauge (C,n)) A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235; let j1, i2 be Element of NAT ; ::_thesis: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) implies [i2,(j1 -' 1)] in Indices (Gauge (C,n)) ) assume that A4: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) ) and A5: [i2,j1] in Indices (Gauge (C,n)) and A6: f /. (len f) = (Gauge (C,n)) * (i2,j1) ; ::_thesis: [i2,(j1 -' 1)] in Indices (Gauge (C,n)) A7: i2 <= len (Gauge (C,n)) by A5, MATRIX_1:38; A8: 1 <= j1 by A5, MATRIX_1:38; A9: now__::_thesis:_not_j1_-'_1_<_1 assume j1 -' 1 < 1 ; ::_thesis: contradiction then j1 <= 1 by NAT_1:14, NAT_D:36; then j1 = 1 by A8, XXREAL_0:1; then cell ((Gauge (C,n)),i2,(1 -' 1)) meets C by A1, A4, A5, A6, A3, GOBRD13:25; then cell ((Gauge (C,n)),i2,0) meets C by XREAL_1:232; hence contradiction by A7, JORDAN8:17; ::_thesis: verum end; A10: j1 -' 1 <= j1 by NAT_D:35; j1 <= width (Gauge (C,n)) by A5, MATRIX_1:38; then A11: j1 -' 1 <= width (Gauge (C,n)) by A10, XXREAL_0:2; 1 <= i2 by A5, MATRIX_1:38; hence [i2,(j1 -' 1)] in Indices (Gauge (C,n)) by A7, A11, A9, MATRIX_1:36; ::_thesis: verum end; theorem :: JORDAN1H:55 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [(i1 + 1),j2] in Indices (Gauge (C,n)) proof let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [(i1 + 1),j2] in Indices (Gauge (C,n)) let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [(i1 + 1),j2] in Indices (Gauge (C,n)) set G = Gauge (C,n); A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [(i1 + 1),j2] in Indices (Gauge (C,n)) ) assume that A2: f is_sequence_on Gauge (C,n) and A3: len f > 1 ; ::_thesis: for i1, j2 being Element of NAT st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [(i1 + 1),j2] in Indices (Gauge (C,n)) A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235; let i1, j2 be Element of NAT ; ::_thesis: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) implies [(i1 + 1),j2] in Indices (Gauge (C,n)) ) assume that A5: ( left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) ) and A6: [i1,j2] in Indices (Gauge (C,n)) and A7: f /. (len f) = (Gauge (C,n)) * (i1,j2) ; ::_thesis: [(i1 + 1),j2] in Indices (Gauge (C,n)) A8: j2 <= width (Gauge (C,n)) by A6, MATRIX_1:38; A9: i1 <= len (Gauge (C,n)) by A6, MATRIX_1:38; A10: now__::_thesis:_not_i1_+_1_>_len_(Gauge_(C,n)) assume i1 + 1 > len (Gauge (C,n)) ; ::_thesis: contradiction then A11: (len (Gauge (C,n))) + 1 <= i1 + 1 by NAT_1:13; i1 + 1 <= (len (Gauge (C,n))) + 1 by A9, XREAL_1:6; then i1 + 1 = (len (Gauge (C,n))) + 1 by A11, XXREAL_0:1; then cell ((Gauge (C,n)),(len (Gauge (C,n))),j2) meets C by A2, A5, A6, A7, A4, GOBRD13:27; hence contradiction by A1, A8, JORDAN8:16; ::_thesis: verum end; A12: 1 <= i1 + 1 by NAT_1:11; 1 <= j2 by A6, MATRIX_1:38; hence [(i1 + 1),j2] in Indices (Gauge (C,n)) by A8, A12, A10, MATRIX_1:36; ::_thesis: verum end; theorem :: JORDAN1H:56 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [i1,(j1 + 2)] in Indices (Gauge (C,n)) proof let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [i1,(j1 + 2)] in Indices (Gauge (C,n)) let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [i1,(j1 + 2)] in Indices (Gauge (C,n)) set G = Gauge (C,n); A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [i1,(j1 + 2)] in Indices (Gauge (C,n)) ) assume that A2: f is_sequence_on Gauge (C,n) and A3: len f > 1 ; ::_thesis: for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [i1,(j1 + 2)] in Indices (Gauge (C,n)) A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235; let i1, j1 be Element of NAT ; ::_thesis: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) implies [i1,(j1 + 2)] in Indices (Gauge (C,n)) ) assume that A5: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) ) and A6: [i1,(j1 + 1)] in Indices (Gauge (C,n)) and A7: f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) ; ::_thesis: [i1,(j1 + 2)] in Indices (Gauge (C,n)) A8: i1 <= len (Gauge (C,n)) by A6, MATRIX_1:38; A9: i1 -' 1 <= i1 by NAT_D:35; A10: j1 + 1 <= width (Gauge (C,n)) by A6, MATRIX_1:38; A11: now__::_thesis:_not_(j1_+_1)_+_1_>_len_(Gauge_(C,n)) assume (j1 + 1) + 1 > len (Gauge (C,n)) ; ::_thesis: contradiction then A12: (len (Gauge (C,n))) + 1 <= (j1 + 1) + 1 by NAT_1:13; (j1 + 1) + 1 <= (len (Gauge (C,n))) + 1 by A1, A10, XREAL_1:6; then (j1 + 1) + 1 = (len (Gauge (C,n))) + 1 by A12, XXREAL_0:1; then cell ((Gauge (C,n)),(i1 -' 1),(len (Gauge (C,n)))) meets C by A2, A5, A6, A7, A4, GOBRD13:34; hence contradiction by A8, A9, JORDAN8:15, XXREAL_0:2; ::_thesis: verum end; A13: 1 <= (j1 + 1) + 1 by NAT_1:12; 1 <= i1 by A6, MATRIX_1:38; hence [i1,(j1 + 2)] in Indices (Gauge (C,n)) by A1, A8, A13, A11, MATRIX_1:36; ::_thesis: verum end; theorem :: JORDAN1H:57 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 2),j1] in Indices (Gauge (C,n)) proof let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 2),j1] in Indices (Gauge (C,n)) let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 2),j1] in Indices (Gauge (C,n)) set G = Gauge (C,n); A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 2),j1] in Indices (Gauge (C,n)) ) assume that A2: f is_sequence_on Gauge (C,n) and A3: len f > 1 ; ::_thesis: for i1, j1 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 2),j1] in Indices (Gauge (C,n)) A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235; let i1, j1 be Element of NAT ; ::_thesis: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) implies [(i1 + 2),j1] in Indices (Gauge (C,n)) ) assume that A5: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) ) and A6: [(i1 + 1),j1] in Indices (Gauge (C,n)) and A7: f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) ; ::_thesis: [(i1 + 2),j1] in Indices (Gauge (C,n)) A8: j1 <= width (Gauge (C,n)) by A6, MATRIX_1:38; A9: i1 + 1 <= len (Gauge (C,n)) by A6, MATRIX_1:38; A10: now__::_thesis:_not_(i1_+_1)_+_1_>_len_(Gauge_(C,n)) assume (i1 + 1) + 1 > len (Gauge (C,n)) ; ::_thesis: contradiction then A11: (len (Gauge (C,n))) + 1 <= (i1 + 1) + 1 by NAT_1:13; (i1 + 1) + 1 <= (len (Gauge (C,n))) + 1 by A9, XREAL_1:6; then (i1 + 1) + 1 = (len (Gauge (C,n))) + 1 by A11, XXREAL_0:1; then cell ((Gauge (C,n)),(len (Gauge (C,n))),j1) meets C by A2, A5, A6, A7, A4, GOBRD13:36; hence contradiction by A1, A8, JORDAN8:16; ::_thesis: verum end; A12: 1 <= (i1 + 1) + 1 by NAT_1:12; 1 <= j1 by A6, MATRIX_1:38; hence [(i1 + 2),j1] in Indices (Gauge (C,n)) by A8, A12, A10, MATRIX_1:36; ::_thesis: verum end; theorem :: JORDAN1H:58 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for j1, i2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [(i2 -' 1),j1] in Indices (Gauge (C,n)) proof let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for j1, i2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [(i2 -' 1),j1] in Indices (Gauge (C,n)) let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for j1, i2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [(i2 -' 1),j1] in Indices (Gauge (C,n)) set G = Gauge (C,n); A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for j1, i2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [(i2 -' 1),j1] in Indices (Gauge (C,n)) ) assume that A2: f is_sequence_on Gauge (C,n) and A3: len f > 1 ; ::_thesis: for j1, i2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [(i2 -' 1),j1] in Indices (Gauge (C,n)) A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235; let j1, i2 be Element of NAT ; ::_thesis: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) implies [(i2 -' 1),j1] in Indices (Gauge (C,n)) ) assume that A5: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) ) and A6: [i2,j1] in Indices (Gauge (C,n)) and A7: f /. (len f) = (Gauge (C,n)) * (i2,j1) ; ::_thesis: [(i2 -' 1),j1] in Indices (Gauge (C,n)) A8: j1 <= width (Gauge (C,n)) by A6, MATRIX_1:38; A9: 1 <= i2 by A6, MATRIX_1:38; A10: now__::_thesis:_not_i2_-'_1_<_1 assume i2 -' 1 < 1 ; ::_thesis: contradiction then i2 <= 1 by NAT_1:14, NAT_D:36; then i2 = 1 by A9, XXREAL_0:1; then cell ((Gauge (C,n)),(1 -' 1),(j1 -' 1)) meets C by A2, A5, A6, A7, A4, GOBRD13:38; then cell ((Gauge (C,n)),0,(j1 -' 1)) meets C by XREAL_1:232; hence contradiction by A1, A8, JORDAN8:18, NAT_D:44; ::_thesis: verum end; i2 <= len (Gauge (C,n)) by A6, MATRIX_1:38; then A11: i2 -' 1 <= len (Gauge (C,n)) by NAT_D:44; 1 <= j1 by A6, MATRIX_1:38; hence [(i2 -' 1),j1] in Indices (Gauge (C,n)) by A8, A11, A10, MATRIX_1:36; ::_thesis: verum end; theorem :: JORDAN1H:59 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [i1,(j2 -' 1)] in Indices (Gauge (C,n)) proof let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [i1,(j2 -' 1)] in Indices (Gauge (C,n)) let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [i1,(j2 -' 1)] in Indices (Gauge (C,n)) set G = Gauge (C,n); let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [i1,(j2 -' 1)] in Indices (Gauge (C,n)) ) assume that A1: f is_sequence_on Gauge (C,n) and A2: len f > 1 ; ::_thesis: for i1, j2 being Element of NAT st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [i1,(j2 -' 1)] in Indices (Gauge (C,n)) A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235; let i1, j2 be Element of NAT ; ::_thesis: ( front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) implies [i1,(j2 -' 1)] in Indices (Gauge (C,n)) ) assume that A4: front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C and A5: [i1,(j2 + 1)] in Indices (Gauge (C,n)) and A6: f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) and A7: [i1,j2] in Indices (Gauge (C,n)) and A8: f /. (len f) = (Gauge (C,n)) * (i1,j2) ; ::_thesis: [i1,(j2 -' 1)] in Indices (Gauge (C,n)) A9: 1 <= j2 by A7, MATRIX_1:38; A10: i1 <= len (Gauge (C,n)) by A5, MATRIX_1:38; A11: now__::_thesis:_not_j2_-'_1_<_1 assume j2 -' 1 < 1 ; ::_thesis: contradiction then j2 <= 1 by NAT_1:14, NAT_D:36; then j2 = 1 by A9, XXREAL_0:1; then cell ((Gauge (C,n)),i1,(1 -' 1)) meets C by A1, A4, A5, A6, A7, A8, A3, GOBRD13:40; then cell ((Gauge (C,n)),i1,0) meets C by XREAL_1:232; hence contradiction by A10, JORDAN8:17; ::_thesis: verum end; j2 <= width (Gauge (C,n)) by A7, MATRIX_1:38; then A12: j2 -' 1 <= width (Gauge (C,n)) by NAT_D:44; ( 1 <= i1 & i1 <= len (Gauge (C,n)) ) by A7, MATRIX_1:38; hence [i1,(j2 -' 1)] in Indices (Gauge (C,n)) by A12, A11, MATRIX_1:36; ::_thesis: verum end; theorem :: JORDAN1H:60 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) proof let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) set G = Gauge (C,n); A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) ) assume that A2: f is_sequence_on Gauge (C,n) and A3: len f > 1 ; ::_thesis: for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235; let i1, j1 be Element of NAT ; ::_thesis: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) implies [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) ) assume that A5: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) ) and A6: [i1,(j1 + 1)] in Indices (Gauge (C,n)) and A7: f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) ; ::_thesis: [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) A8: j1 + 1 <= width (Gauge (C,n)) by A6, MATRIX_1:38; A9: i1 <= len (Gauge (C,n)) by A6, MATRIX_1:38; A10: now__::_thesis:_not_i1_+_1_>_len_(Gauge_(C,n)) assume i1 + 1 > len (Gauge (C,n)) ; ::_thesis: contradiction then A11: (len (Gauge (C,n))) + 1 <= i1 + 1 by NAT_1:13; i1 + 1 <= (len (Gauge (C,n))) + 1 by A9, XREAL_1:6; then i1 + 1 = (len (Gauge (C,n))) + 1 by A11, XXREAL_0:1; then cell ((Gauge (C,n)),(len (Gauge (C,n))),(j1 + 1)) meets C by A2, A5, A6, A7, A4, GOBRD13:35; hence contradiction by A1, A8, JORDAN8:16; ::_thesis: verum end; A12: 1 <= i1 + 1 by NAT_1:11; 1 <= j1 + 1 by A6, MATRIX_1:38; hence [(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n)) by A8, A12, A10, MATRIX_1:36; ::_thesis: verum end; theorem :: JORDAN1H:61 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n)) proof let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n)) let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n)) set G = Gauge (C,n); let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n)) ) assume that A1: f is_sequence_on Gauge (C,n) and A2: len f > 1 ; ::_thesis: for i1, j1 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n)) A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235; let i1, j1 be Element of NAT ; ::_thesis: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) implies [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n)) ) assume that A4: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) ) and A5: [(i1 + 1),j1] in Indices (Gauge (C,n)) and A6: f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) ; ::_thesis: [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n)) A7: i1 + 1 <= len (Gauge (C,n)) by A5, MATRIX_1:38; A8: 1 <= j1 by A5, MATRIX_1:38; A9: now__::_thesis:_not_j1_-'_1_<_1 assume j1 -' 1 < 1 ; ::_thesis: contradiction then j1 <= 1 by NAT_1:14, NAT_D:36; then j1 = 1 by A8, XXREAL_0:1; then cell ((Gauge (C,n)),(i1 + 1),(1 -' 1)) meets C by A1, A4, A5, A6, A3, GOBRD13:37; then cell ((Gauge (C,n)),(i1 + 1),0) meets C by XREAL_1:232; hence contradiction by A7, JORDAN8:17; ::_thesis: verum end; A10: j1 -' 1 <= j1 by NAT_D:35; j1 <= width (Gauge (C,n)) by A5, MATRIX_1:38; then A11: j1 -' 1 <= width (Gauge (C,n)) by A10, XXREAL_0:2; 1 <= i1 + 1 by A5, MATRIX_1:38; hence [(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n)) by A7, A11, A9, MATRIX_1:36; ::_thesis: verum end; theorem :: JORDAN1H:62 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for j1, i2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [i2,(j1 + 1)] in Indices (Gauge (C,n)) proof let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for j1, i2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [i2,(j1 + 1)] in Indices (Gauge (C,n)) let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for j1, i2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [i2,(j1 + 1)] in Indices (Gauge (C,n)) set G = Gauge (C,n); let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for j1, i2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [i2,(j1 + 1)] in Indices (Gauge (C,n)) ) assume that A1: f is_sequence_on Gauge (C,n) and A2: len f > 1 ; ::_thesis: for j1, i2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds [i2,(j1 + 1)] in Indices (Gauge (C,n)) A3: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A2, NAT_D:49, XREAL_1:235; A4: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; let j1, i2 be Element of NAT ; ::_thesis: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) implies [i2,(j1 + 1)] in Indices (Gauge (C,n)) ) assume that A5: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) ) and A6: [i2,j1] in Indices (Gauge (C,n)) and A7: f /. (len f) = (Gauge (C,n)) * (i2,j1) ; ::_thesis: [i2,(j1 + 1)] in Indices (Gauge (C,n)) A8: i2 <= len (Gauge (C,n)) by A6, MATRIX_1:38; A9: j1 <= width (Gauge (C,n)) by A6, MATRIX_1:38; A10: now__::_thesis:_not_j1_+_1_>_len_(Gauge_(C,n)) assume j1 + 1 > len (Gauge (C,n)) ; ::_thesis: contradiction then A11: (len (Gauge (C,n))) + 1 <= j1 + 1 by NAT_1:13; j1 + 1 <= (len (Gauge (C,n))) + 1 by A9, A4, XREAL_1:6; then j1 + 1 = (len (Gauge (C,n))) + 1 by A11, XXREAL_0:1; then cell ((Gauge (C,n)),(i2 -' 1),(len (Gauge (C,n)))) meets C by A1, A5, A6, A7, A3, GOBRD13:39; hence contradiction by A8, JORDAN8:15, NAT_D:44; ::_thesis: verum end; A12: 1 <= j1 + 1 by NAT_1:11; 1 <= i2 by A6, MATRIX_1:38; hence [i2,(j1 + 1)] in Indices (Gauge (C,n)) by A8, A12, A4, A10, MATRIX_1:36; ::_thesis: verum end; theorem :: JORDAN1H:63 for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [(i1 -' 1),j2] in Indices (Gauge (C,n)) proof let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [(i1 -' 1),j2] in Indices (Gauge (C,n)) let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds for i1, j2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [(i1 -' 1),j2] in Indices (Gauge (C,n)) set G = Gauge (C,n); A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_sequence_on Gauge (C,n) & len f > 1 implies for i1, j2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [(i1 -' 1),j2] in Indices (Gauge (C,n)) ) assume that A2: f is_sequence_on Gauge (C,n) and A3: len f > 1 ; ::_thesis: for i1, j2 being Element of NAT st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds [(i1 -' 1),j2] in Indices (Gauge (C,n)) A4: ( 1 <= (len f) -' 1 & ((len f) -' 1) + 1 = len f ) by A3, NAT_D:49, XREAL_1:235; let i1, j2 be Element of NAT ; ::_thesis: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) implies [(i1 -' 1),j2] in Indices (Gauge (C,n)) ) assume that A5: ( front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) ) and A6: [i1,j2] in Indices (Gauge (C,n)) and A7: f /. (len f) = (Gauge (C,n)) * (i1,j2) ; ::_thesis: [(i1 -' 1),j2] in Indices (Gauge (C,n)) A8: j2 <= width (Gauge (C,n)) by A6, MATRIX_1:38; A9: 1 <= i1 by A6, MATRIX_1:38; A10: now__::_thesis:_not_i1_-'_1_<_1 assume i1 -' 1 < 1 ; ::_thesis: contradiction then i1 <= 1 by NAT_1:14, NAT_D:36; then i1 = 1 by A9, XXREAL_0:1; then cell ((Gauge (C,n)),(1 -' 1),(j2 -' 1)) meets C by A2, A5, A6, A7, A4, GOBRD13:41; then cell ((Gauge (C,n)),0,(j2 -' 1)) meets C by XREAL_1:232; hence contradiction by A1, A8, JORDAN8:18, NAT_D:44; ::_thesis: verum end; i1 <= len (Gauge (C,n)) by A6, MATRIX_1:38; then A11: i1 -' 1 <= len (Gauge (C,n)) by NAT_D:44; 1 <= j2 by A6, MATRIX_1:38; hence [(i1 -' 1),j2] in Indices (Gauge (C,n)) by A8, A11, A10, MATRIX_1:36; ::_thesis: verum end;