:: JORDAN1D semantic presentation begin 1 = (2 * 0) + 1 ; then Lm1: 1 div 2 = 0 by NAT_D:def_1; 2 = (2 * 1) + 0 ; then Lm2: 2 div 2 = 1 by NAT_D:def_1; Lm3: for x, A, B, C, D being set holds ( x in ((A \/ B) \/ C) \/ D iff ( x in A or x in B or x in C or x in D ) ) proof let x, A, B, C, D be set ; ::_thesis: ( x in ((A \/ B) \/ C) \/ D iff ( x in A or x in B or x in C or x in D ) ) hereby ::_thesis: ( ( x in A or x in B or x in C or x in D ) implies x in ((A \/ B) \/ C) \/ D ) assume x in ((A \/ B) \/ C) \/ D ; ::_thesis: ( x in A or x in B or x in C or x in D ) then ( x in (A \/ B) \/ C or x in D ) by XBOOLE_0:def_3; then ( x in A \/ B or x in C or x in D ) by XBOOLE_0:def_3; hence ( x in A or x in B or x in C or x in D ) by XBOOLE_0:def_3; ::_thesis: verum end; assume ( x in A or x in B or x in C or x in D ) ; ::_thesis: x in ((A \/ B) \/ C) \/ D then ( x in A \/ B or x in C or x in D ) by XBOOLE_0:def_3; then ( x in (A \/ B) \/ C or x in D ) by XBOOLE_0:def_3; hence x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def_3; ::_thesis: verum end; Lm4: for A, B, C, D being set holds union {A,B,C,D} = ((A \/ B) \/ C) \/ D proof let A, B, C, D be set ; ::_thesis: union {A,B,C,D} = ((A \/ B) \/ C) \/ D A1: B in {A,B,C,D} by ENUMSET1:def_2; A2: D in {A,B,C,D} by ENUMSET1:def_2; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ((A \/ B) \/ C) \/ D c= union {A,B,C,D} let x be set ; ::_thesis: ( x in union {A,B,C,D} implies x in ((A \/ B) \/ C) \/ D ) assume x in union {A,B,C,D} ; ::_thesis: x in ((A \/ B) \/ C) \/ D then consider Z being set such that A3: x in Z and A4: Z in {A,B,C,D} by TARSKI:def_4; ( Z = A or Z = B or Z = C or Z = D ) by A4, ENUMSET1:def_2; hence x in ((A \/ B) \/ C) \/ D by A3, Lm3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((A \/ B) \/ C) \/ D or x in union {A,B,C,D} ) A5: C in {A,B,C,D} by ENUMSET1:def_2; assume x in ((A \/ B) \/ C) \/ D ; ::_thesis: x in union {A,B,C,D} then A6: ( x in A or x in B or x in C or x in D ) by Lm3; A in {A,B,C,D} by ENUMSET1:def_2; hence x in union {A,B,C,D} by A6, A1, A5, A2, TARSKI:def_4; ::_thesis: verum end; theorem Th1: :: JORDAN1D:1 for A, B being set st ( for x being set st x in A holds ex K being set st ( K c= B & x c= union K ) ) holds union A c= union B proof let A, B be set ; ::_thesis: ( ( for x being set st x in A holds ex K being set st ( K c= B & x c= union K ) ) implies union A c= union B ) assume A1: for x being set st x in A holds ex K being set st ( K c= B & x c= union K ) ; ::_thesis: union A c= union B let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union A or a in union B ) assume a in union A ; ::_thesis: a in union B then consider Z being set such that A2: a in Z and A3: Z in A by TARSKI:def_4; consider K being set such that A4: K c= B and A5: Z c= union K by A1, A3; ex S being set st ( a in S & S in K ) by A2, A5, TARSKI:def_4; hence a in union B by A4, TARSKI:def_4; ::_thesis: verum end; registration let m be non empty Element of NAT ; cluster2 |^ m -> even ; coherence 2 |^ m is even proof defpred S1[ Nat] means ( not m is empty implies 2 |^ m is even ); A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume that S1[k] and not k + 1 is empty ; ::_thesis: 2 |^ (k + 1) is even 2 |^ (k + 1) = 2 * (2 |^ k) by NEWTON:6; hence 2 |^ (k + 1) is even ; ::_thesis: verum end; A2: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A2, A1); hence 2 |^ m is even ; ::_thesis: verum end; end; registration let n be even Element of NAT ; let m be non empty Element of NAT ; clustern |^ m -> even ; coherence n |^ m is even proof defpred S1[ Element of NAT ] means ( not n is empty implies n |^ n is even ); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume that S1[k] and not k + 1 is empty ; ::_thesis: n |^ (k + 1) is even n |^ (k + 1) = n * (n |^ k) by NEWTON:6; hence n |^ (k + 1) is even ; ::_thesis: verum end; A2: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A1); hence n |^ m is even ; ::_thesis: verum end; end; theorem Th2: :: JORDAN1D:2 for i being Element of NAT for r being real number st r <> 0 holds (1 / r) * (r |^ (i + 1)) = r |^ i proof let i be Element of NAT ; ::_thesis: for r being real number st r <> 0 holds (1 / r) * (r |^ (i + 1)) = r |^ i let r be real number ; ::_thesis: ( r <> 0 implies (1 / r) * (r |^ (i + 1)) = r |^ i ) assume A1: r <> 0 ; ::_thesis: (1 / r) * (r |^ (i + 1)) = r |^ i thus (1 / r) * (r |^ (i + 1)) = (1 / r) * ((r |^ i) * r) by NEWTON:6 .= ((1 / r) * r) * (r |^ i) .= 1 * (r |^ i) by A1, XCMPLX_1:106 .= r |^ i ; ::_thesis: verum end; Lm5: now__::_thesis:_for_m_being_real_number_st_2_<=_m_holds_ (2_*_m)_-_2_>=_0 let m be real number ; ::_thesis: ( 2 <= m implies (2 * m) - 2 >= 0 ) assume 2 <= m ; ::_thesis: (2 * m) - 2 >= 0 then 2 * m >= 2 * 2 by XREAL_1:66; then (2 * m) - 2 >= 4 - 2 by XREAL_1:9; hence (2 * m) - 2 >= 0 ; ::_thesis: verum end; Lm6: now__::_thesis:_for_m_being_real_number_st_1_<=_m_holds_ (2_*_m)_-_1_>=_0 let m be real number ; ::_thesis: ( 1 <= m implies (2 * m) - 1 >= 0 ) assume 1 <= m ; ::_thesis: (2 * m) - 1 >= 0 then 2 * m >= 2 * 1 by XREAL_1:66; then (2 * m) - 1 >= 2 - 1 by XREAL_1:9; hence (2 * m) - 1 >= 0 ; ::_thesis: verum end; Lm7: now__::_thesis:_for_m_being_Element_of_NAT_st_2_<=_m_holds_ (2_*_m)_-_2_=_(2_*_m)_-'_2 let m be Element of NAT ; ::_thesis: ( 2 <= m implies (2 * m) - 2 = (2 * m) -' 2 ) assume 2 <= m ; ::_thesis: (2 * m) - 2 = (2 * m) -' 2 then (2 * m) - 2 >= 0 by Lm5; hence (2 * m) - 2 = (2 * m) -' 2 by XREAL_0:def_2; ::_thesis: verum end; Lm8: now__::_thesis:_for_m_being_Element_of_NAT_st_1_<=_m_holds_ (2_*_m)_-_1_=_(2_*_m)_-'_1 let m be Element of NAT ; ::_thesis: ( 1 <= m implies (2 * m) - 1 = (2 * m) -' 1 ) assume 1 <= m ; ::_thesis: (2 * m) - 1 = (2 * m) -' 1 then (2 * m) - 1 >= 0 by Lm6; hence (2 * m) - 1 = (2 * m) -' 1 by XREAL_0:def_2; ::_thesis: verum end; Lm9: now__::_thesis:_for_m_being_Element_of_NAT_st_m_>=_1_holds_ ((2_*_m)_-'_2)_+_1_=_(2_*_m)_-'_1 let m be Element of NAT ; ::_thesis: ( m >= 1 implies ((2 * m) -' 2) + 1 = (2 * m) -' 1 ) assume A1: m >= 1 ; ::_thesis: ((2 * m) -' 2) + 1 = (2 * m) -' 1 then 2 * m >= 2 * 1 by XREAL_1:64; then (2 * m) - 1 >= 2 - 1 by XREAL_1:9; then A2: (2 * m) -' 1 >= 1 by A1, Lm8; thus ((2 * m) -' 2) + 1 = (((2 * m) -' 1) -' 1) + 1 by NAT_D:45 .= (2 * m) -' 1 by A2, XREAL_1:235 ; ::_thesis: verum end; Lm10: for m, i being Element of NAT for x being real number st 2 <= m holds (x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2) proof let m, i be Element of NAT ; ::_thesis: for x being real number st 2 <= m holds (x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2) let x be real number ; ::_thesis: ( 2 <= m implies (x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2) ) assume 2 <= m ; ::_thesis: (x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2) then A1: (2 * m) - 2 >= 0 by Lm5; thus (x / (2 |^ i)) * (m - 2) = x / ((2 |^ i) / (m - 2)) by XCMPLX_1:81 .= x / (((2 |^ i) * 2) / ((m - 2) * 2)) by XCMPLX_1:91 .= (x / ((2 |^ i) * 2)) * ((m - 2) * 2) by XCMPLX_1:81 .= (x / (2 |^ (i + 1))) * (((2 * m) - 2) - 2) by NEWTON:6 .= (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2) by A1, XREAL_0:def_2 ; ::_thesis: verum end; Lm11: for m being Element of NAT st 2 <= m holds 1 <= (2 * m) -' 2 proof let m be Element of NAT ; ::_thesis: ( 2 <= m implies 1 <= (2 * m) -' 2 ) assume A1: 2 <= m ; ::_thesis: 1 <= (2 * m) -' 2 then 2 * 2 <= 2 * m by XREAL_1:66; then A2: 4 - 2 <= (2 * m) - 2 by XREAL_1:9; (2 * m) -' 2 = (2 * m) - 2 by A1, Lm7; hence 1 <= (2 * m) -' 2 by A2, XXREAL_0:2; ::_thesis: verum end; Lm12: for m being Element of NAT st 1 <= m holds 1 <= (2 * m) -' 1 proof let m be Element of NAT ; ::_thesis: ( 1 <= m implies 1 <= (2 * m) -' 1 ) assume A1: 1 <= m ; ::_thesis: 1 <= (2 * m) -' 1 then 2 * 1 <= 2 * m by XREAL_1:66; then 2 - 1 <= (2 * m) - 1 by XREAL_1:9; hence 1 <= (2 * m) -' 1 by A1, Lm8; ::_thesis: verum end; Lm13: for m, i being Element of NAT st m < (2 |^ i) + 3 holds (2 * m) -' 2 < (2 |^ (i + 1)) + 3 proof let m, i be Element of NAT ; ::_thesis: ( m < (2 |^ i) + 3 implies (2 * m) -' 2 < (2 |^ (i + 1)) + 3 ) percases ( m = 0 or m = 1 or 2 <= m ) by NAT_1:26; suppose ( m = 0 or m = 1 ) ; ::_thesis: ( m < (2 |^ i) + 3 implies (2 * m) -' 2 < (2 |^ (i + 1)) + 3 ) hence ( m < (2 |^ i) + 3 implies (2 * m) -' 2 < (2 |^ (i + 1)) + 3 ) by NAT_2:8; ::_thesis: verum end; supposeA1: 2 <= m ; ::_thesis: ( m < (2 |^ i) + 3 implies (2 * m) -' 2 < (2 |^ (i + 1)) + 3 ) assume m < (2 |^ i) + 3 ; ::_thesis: (2 * m) -' 2 < (2 |^ (i + 1)) + 3 then m + 1 <= (2 |^ i) + 3 by NAT_1:13; then 2 * (m + 1) <= 2 * ((2 |^ i) + 3) by XREAL_1:64; then (2 * m) + (2 * 1) <= (2 * (2 |^ i)) + (2 * 3) ; then (2 * m) + (2 * 1) <= (2 |^ (i + 1)) + 6 by NEWTON:6; then ((2 * m) + 2) - 4 <= ((2 |^ (i + 1)) + 6) - 4 by XREAL_1:9; then (2 * m) - 2 <= (2 |^ (i + 1)) + 2 ; then A2: (2 * m) -' 2 <= (2 |^ (i + 1)) + 2 by A1, Lm7; (2 |^ (i + 1)) + 2 < (2 |^ (i + 1)) + 3 by XREAL_1:6; hence (2 * m) -' 2 < (2 |^ (i + 1)) + 3 by A2, XXREAL_0:2; ::_thesis: verum end; end; end; Lm14: now__::_thesis:_for_m_being_Element_of_NAT_st_2_<=_m_holds_ (((2_*_m)_-'_2)_+_1)_-_2_=_(2_*_m)_-_3 let m be Element of NAT ; ::_thesis: ( 2 <= m implies (((2 * m) -' 2) + 1) - 2 = (2 * m) - 3 ) assume 2 <= m ; ::_thesis: (((2 * m) -' 2) + 1) - 2 = (2 * m) - 3 hence (((2 * m) -' 2) + 1) - 2 = (((2 * m) - 2) + 1) - 2 by Lm7 .= (2 * m) - 3 ; ::_thesis: verum end; begin theorem Th3: :: JORDAN1D:3 for m, i, a, b being Element of NAT for D being non empty Subset of (TOP-REAL 2) st 2 <= m & m < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) holds ((Gauge (D,i)) * (m,a)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1 proof let m, i, a, b be Element of NAT ; ::_thesis: for D being non empty Subset of (TOP-REAL 2) st 2 <= m & m < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) holds ((Gauge (D,i)) * (m,a)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1 let D be non empty Subset of (TOP-REAL 2); ::_thesis: ( 2 <= m & m < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) implies ((Gauge (D,i)) * (m,a)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1 ) set I = Gauge (D,i); set J = Gauge (D,(i + 1)); set z = N-bound D; set e = E-bound D; set s = S-bound D; set w = W-bound D; assume that A1: 2 <= m and A2: m < len (Gauge (D,i)) and A3: 1 <= a and A4: a <= len (Gauge (D,i)) and A5: 1 <= b and A6: b <= len (Gauge (D,(i + 1))) ; ::_thesis: ((Gauge (D,i)) * (m,a)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1 m < (2 |^ i) + 3 by A2, JORDAN8:def_1; then (2 * m) -' 2 <= (2 |^ (i + 1)) + 3 by Lm13; then A7: (2 * m) -' 2 <= len (Gauge (D,(i + 1))) by JORDAN8:def_1; A8: len (Gauge (D,(i + 1))) = width (Gauge (D,(i + 1))) by JORDAN8:def_1; 1 <= (2 * m) -' 2 by A1, Lm11; then A9: [((2 * m) -' 2),b] in Indices (Gauge (D,(i + 1))) by A5, A6, A8, A7, MATRIX_1:36; A10: len (Gauge (D,i)) = width (Gauge (D,i)) by JORDAN8:def_1; 1 <= m by A1, XXREAL_0:2; then [m,a] in Indices (Gauge (D,i)) by A2, A3, A4, A10, MATRIX_1:36; hence ((Gauge (D,i)) * (m,a)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * (m - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * (a - 2)))]| `1 by JORDAN8:def_1 .= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * (m - 2)) by EUCLID:52 .= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2)) by A1, Lm10 .= |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (b - 2)))]| `1 by EUCLID:52 .= ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1 by A9, JORDAN8:def_1 ; ::_thesis: verum end; theorem Th4: :: JORDAN1D:4 for n, i, a, b being Element of NAT for D being non empty Subset of (TOP-REAL 2) st 2 <= n & n < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) holds ((Gauge (D,i)) * (a,n)) `2 = ((Gauge (D,(i + 1))) * (b,((2 * n) -' 2))) `2 proof let n, i, a, b be Element of NAT ; ::_thesis: for D being non empty Subset of (TOP-REAL 2) st 2 <= n & n < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) holds ((Gauge (D,i)) * (a,n)) `2 = ((Gauge (D,(i + 1))) * (b,((2 * n) -' 2))) `2 let D be non empty Subset of (TOP-REAL 2); ::_thesis: ( 2 <= n & n < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) implies ((Gauge (D,i)) * (a,n)) `2 = ((Gauge (D,(i + 1))) * (b,((2 * n) -' 2))) `2 ) set I = Gauge (D,i); set J = Gauge (D,(i + 1)); set z = N-bound D; set e = E-bound D; set s = S-bound D; set w = W-bound D; assume that A1: 2 <= n and A2: n < len (Gauge (D,i)) and A3: 1 <= a and A4: a <= len (Gauge (D,i)) and A5: 1 <= b and A6: b <= len (Gauge (D,(i + 1))) ; ::_thesis: ((Gauge (D,i)) * (a,n)) `2 = ((Gauge (D,(i + 1))) * (b,((2 * n) -' 2))) `2 n < (2 |^ i) + 3 by A2, JORDAN8:def_1; then (2 * n) -' 2 <= (2 |^ (i + 1)) + 3 by Lm13; then A7: (2 * n) -' 2 <= len (Gauge (D,(i + 1))) by JORDAN8:def_1; A8: len (Gauge (D,(i + 1))) = width (Gauge (D,(i + 1))) by JORDAN8:def_1; 1 <= (2 * n) -' 2 by A1, Lm11; then A9: [b,((2 * n) -' 2)] in Indices (Gauge (D,(i + 1))) by A5, A6, A8, A7, MATRIX_1:36; A10: len (Gauge (D,i)) = width (Gauge (D,i)) by JORDAN8:def_1; 1 <= n by A1, XXREAL_0:2; then [a,n] in Indices (Gauge (D,i)) by A2, A3, A4, A10, MATRIX_1:36; hence ((Gauge (D,i)) * (a,n)) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * (a - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * (n - 2)))]| `2 by JORDAN8:def_1 .= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * (n - 2)) by EUCLID:52 .= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (((2 * n) -' 2) - 2)) by A1, Lm10 .= |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (b - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (((2 * n) -' 2) - 2)))]| `2 by EUCLID:52 .= ((Gauge (D,(i + 1))) * (b,((2 * n) -' 2))) `2 by A9, JORDAN8:def_1 ; ::_thesis: verum end; Lm15: for m, i being Element of NAT for D being non empty Subset of (TOP-REAL 2) st m + 1 < len (Gauge (D,i)) holds (2 * m) -' 1 < len (Gauge (D,(i + 1))) proof let m, i be Element of NAT ; ::_thesis: for D being non empty Subset of (TOP-REAL 2) st m + 1 < len (Gauge (D,i)) holds (2 * m) -' 1 < len (Gauge (D,(i + 1))) let D be non empty Subset of (TOP-REAL 2); ::_thesis: ( m + 1 < len (Gauge (D,i)) implies (2 * m) -' 1 < len (Gauge (D,(i + 1))) ) assume m + 1 < len (Gauge (D,i)) ; ::_thesis: (2 * m) -' 1 < len (Gauge (D,(i + 1))) then m + 1 < (2 |^ i) + 3 by JORDAN8:def_1; then (2 * (m + 1)) -' 2 < (2 |^ (i + 1)) + 3 by Lm13; then ((2 * m) + (2 * 1)) -' 2 < (2 |^ (i + 1)) + 3 ; then A1: 2 * m < (2 |^ (i + 1)) + 3 by NAT_D:34; (2 * m) -' 1 <= 2 * m by NAT_D:44; then (2 * m) -' 1 < (2 |^ (i + 1)) + 3 by A1, XXREAL_0:2; hence (2 * m) -' 1 < len (Gauge (D,(i + 1))) by JORDAN8:def_1; ::_thesis: verum end; theorem Th5: :: JORDAN1D:5 for m, i, n being Element of NAT for D being compact non horizontal non vertical Subset of (TOP-REAL 2) st 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) holds cell ((Gauge (D,i)),m,n) = (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) proof let m, i, n be Element of NAT ; ::_thesis: for D being compact non horizontal non vertical Subset of (TOP-REAL 2) st 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) holds cell ((Gauge (D,i)),m,n) = (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) let D be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) implies cell ((Gauge (D,i)),m,n) = (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) ) set I = Gauge (D,i); set J = Gauge (D,(i + 1)); set z = N-bound D; set e = E-bound D; set s = S-bound D; set w = W-bound D; assume that A1: 2 <= m and A2: m + 1 < len (Gauge (D,i)) and A3: 2 <= n and A4: n + 1 < len (Gauge (D,i)) ; ::_thesis: cell ((Gauge (D,i)),m,n) = (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) A5: len (Gauge (D,(i + 1))) = width (Gauge (D,(i + 1))) by JORDAN8:def_1; A6: (2 * n) - 3 < (2 * n) - 2 by XREAL_1:15; (N-bound D) - (S-bound D) >= 0 by SPRECT_1:22, XREAL_1:48; then (((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 3) <= (((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 2) by A6, XREAL_1:64; then A7: (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 3)) <= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 2)) by XREAL_1:6; A8: m <= m + 1 by NAT_1:11; A9: ((2 * (n + 1)) -' 2) - 2 = (((2 * n) + (2 * 1)) -' 2) - 2 .= (2 * n) - 2 by NAT_D:34 ; A10: 1 <= ((2 * m) -' 2) + 1 by NAT_1:11; A11: 1 <= len (Gauge (D,(i + 1))) by GOBRD11:34; A12: 1 <= n by A3, XXREAL_0:2; then A13: 1 <= (2 * n) -' 1 by Lm12; (2 * n) -' 1 <= 2 * n by NAT_D:35; then A14: 1 <= 2 * n by A13, XXREAL_0:2; A15: ((2 * n) -' 1) + 1 = 2 * n by A12, Lm12, NAT_D:43; A16: (2 * n) -' 1 < len (Gauge (D,(i + 1))) by A4, Lm15; then ((2 * n) -' 1) + 1 <= len (Gauge (D,(i + 1))) by NAT_1:13; then [1,(2 * n)] in Indices (Gauge (D,(i + 1))) by A5, A15, A11, A14, MATRIX_1:36; then A17: ((Gauge (D,(i + 1))) * (1,(2 * n))) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 2)))]| `2 by JORDAN8:def_1 .= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((2 * n) - 2)) by EUCLID:52 ; A18: (2 * m) -' 1 = (2 * m) - 1 by A1, Lm8, XXREAL_0:2; A19: (((2 * m) -' 2) + 1) - 2 = (2 * m) - 3 by A1, Lm14; A20: 1 <= ((2 * n) -' 2) + 1 by NAT_1:11; A21: (2 * m) -' 1 < len (Gauge (D,(i + 1))) by A2, Lm15; A22: n <= n + 1 by NAT_1:11; A23: ((2 * n) -' 2) + 1 = (2 * n) -' 1 by A3, Lm9, XXREAL_0:2; A24: ((2 * (m + 1)) -' 2) - 2 = (((2 * m) + (2 * 1)) -' 2) - 2 .= (2 * m) - 2 by NAT_D:34 ; A25: m < len (Gauge (D,i)) by A2, NAT_1:13; then m < (2 |^ i) + 3 by JORDAN8:def_1; then (2 * m) -' 2 < (2 |^ (i + 1)) + 3 by Lm13; then A26: (2 * m) -' 2 < len (Gauge (D,(i + 1))) by JORDAN8:def_1; then ((2 * m) -' 2) + 1 <= len (Gauge (D,(i + 1))) by NAT_1:13; then [(((2 * m) -' 2) + 1),1] in Indices (Gauge (D,(i + 1))) by A5, A11, A10, MATRIX_1:36; then A27: ((Gauge (D,(i + 1))) * ((((2 * m) -' 2) + 1),1)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((((2 * m) -' 2) + 1) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (1 - 2)))]| `1 by JORDAN8:def_1 .= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((((2 * m) -' 2) + 1) - 2)) by EUCLID:52 ; A28: 1 <= m by A1, XXREAL_0:2; then A29: 1 < len (Gauge (D,i)) by A25, XXREAL_0:2; then A30: ((Gauge (D,i)) * (m,1)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),1)) `1 by A1, A25, A11, Th3; A31: len (Gauge (D,i)) = width (Gauge (D,i)) by JORDAN8:def_1; then A32: n < width (Gauge (D,i)) by A4, NAT_1:13; then A33: ((Gauge (D,i)) * (1,n)) `2 = ((Gauge (D,(i + 1))) * (1,((2 * n) -' 2))) `2 by A3, A31, A29, A11, Th4; A34: 1 <= (2 * m) -' 2 by A1, Lm11; then A35: cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)) = { |[r,q]| where r, q is Real : ( ((Gauge (D,(i + 1))) * (((2 * m) -' 2),1)) `1 <= r & r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 2) + 1),1)) `1 & ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 <= q & q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 1) + 1))) `2 ) } by A5, A13, A26, A16, GOBRD11:32; (2 * m) -' 2 = (2 * m) - 2 by A1, Lm7; then (2 * m) -' 2 < (2 * m) -' 1 by A18, XREAL_1:15; then A36: ((Gauge (D,(i + 1))) * (((2 * m) -' 2),1)) `1 < ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 by A5, A11, A34, A21, GOBOARD5:3; A37: (2 * n) -' 1 = (2 * n) - 1 by A3, Lm8, XXREAL_0:2; A38: (((2 * n) -' 2) + 1) - 2 = (2 * n) - 3 by A3, Lm14; n < (2 |^ i) + 3 by A31, A32, JORDAN8:def_1; then (2 * n) -' 2 < (2 |^ (i + 1)) + 3 by Lm13; then A39: (2 * n) -' 2 < width (Gauge (D,(i + 1))) by A5, JORDAN8:def_1; then ((2 * n) -' 2) + 1 <= len (Gauge (D,(i + 1))) by A5, NAT_1:13; then [1,(((2 * n) -' 2) + 1)] in Indices (Gauge (D,(i + 1))) by A5, A11, A20, MATRIX_1:36; then A40: ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 2) + 1))) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((((2 * n) -' 2) + 1) - 2)))]| `2 by JORDAN8:def_1 .= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * ((((2 * n) -' 2) + 1) - 2)) by EUCLID:52 ; A41: 1 <= (2 * n) -' 2 by A3, Lm11; then A42: cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2)) = { |[r,q]| where r, q is Real : ( ((Gauge (D,(i + 1))) * (((2 * m) -' 2),1)) `1 <= r & r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 2) + 1),1)) `1 & ((Gauge (D,(i + 1))) * (1,((2 * n) -' 2))) `2 <= q & q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 2) + 1))) `2 ) } by A34, A26, A39, GOBRD11:32; A43: 1 <= (2 * m) -' 1 by A28, Lm12; then A44: cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)) = { |[r,q]| where r, q is Real : ( ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 <= r & r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 1) + 1),1)) `1 & ((Gauge (D,(i + 1))) * (1,((2 * n) -' 2))) `2 <= q & q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 2) + 1))) `2 ) } by A41, A39, A21, GOBRD11:32; A45: cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)) = { |[r,q]| where r, q is Real : ( ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 <= r & r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 1) + 1),1)) `1 & ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 <= q & q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 1) + 1))) `2 ) } by A5, A13, A43, A16, A21, GOBRD11:32; A46: cell ((Gauge (D,i)),m,n) = { |[r,q]| where r, q is Real : ( ((Gauge (D,i)) * (m,1)) `1 <= r & r <= ((Gauge (D,i)) * ((m + 1),1)) `1 & ((Gauge (D,i)) * (1,n)) `2 <= q & q <= ((Gauge (D,i)) * (1,(n + 1))) `2 ) } by A28, A12, A25, A32, GOBRD11:32; 1 <= n + 1 by NAT_1:11; then [1,(n + 1)] in Indices (Gauge (D,i)) by A4, A31, A29, MATRIX_1:36; then A47: ((Gauge (D,i)) * (1,(n + 1))) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * ((n + 1) - 2)))]| `2 by JORDAN8:def_1 .= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * ((n + 1) - 2)) by EUCLID:52 .= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (((2 * (n + 1)) -' 2) - 2)) by A3, A22, Lm10, XXREAL_0:2 ; 1 <= m + 1 by NAT_1:11; then [(m + 1),1] in Indices (Gauge (D,i)) by A2, A31, A29, MATRIX_1:36; then A48: ((Gauge (D,i)) * ((m + 1),1)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * ((m + 1) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * (1 - 2)))]| `1 by JORDAN8:def_1 .= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * ((m + 1) - 2)) by EUCLID:52 .= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (((2 * (m + 1)) -' 2) - 2)) by A1, A8, Lm10, XXREAL_0:2 ; (2 * n) -' 2 = (2 * n) - 2 by A3, Lm7; then (2 * n) -' 2 < (2 * n) -' 1 by A37, XREAL_1:15; then A49: ((Gauge (D,(i + 1))) * (1,((2 * n) -' 2))) `2 < ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 by A5, A11, A41, A16, GOBOARD5:4; A50: ((2 * m) -' 1) + 1 = 2 * m by A28, Lm12, NAT_D:43; (2 * m) -' 1 <= 2 * m by NAT_D:35; then A51: 1 <= 2 * m by A43, XXREAL_0:2; ((2 * m) -' 1) + 1 <= len (Gauge (D,(i + 1))) by A21, NAT_1:13; then [(2 * m),1] in Indices (Gauge (D,(i + 1))) by A5, A50, A11, A51, MATRIX_1:36; then A52: ((Gauge (D,(i + 1))) * ((2 * m),1)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (1 - 2)))]| `1 by JORDAN8:def_1 .= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 2)) by EUCLID:52 ; A53: ((2 * m) -' 2) + 1 = (2 * m) -' 1 by A1, Lm9, XXREAL_0:2; thus cell ((Gauge (D,i)),m,n) c= (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) :: according to XBOOLE_0:def_10 ::_thesis: (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) c= cell ((Gauge (D,i)),m,n) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell ((Gauge (D,i)),m,n) or x in (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) ) assume x in cell ((Gauge (D,i)),m,n) ; ::_thesis: x in (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) then consider r, q being Real such that A54: x = |[r,q]| and A55: ((Gauge (D,i)) * (m,1)) `1 <= r and A56: r <= ((Gauge (D,i)) * ((m + 1),1)) `1 and A57: ((Gauge (D,i)) * (1,n)) `2 <= q and A58: q <= ((Gauge (D,i)) * (1,(n + 1))) `2 by A46; ( ( r <= ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 & q <= ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 ) or ( r >= ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 & q <= ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 ) or ( r <= ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 & q >= ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 ) or ( r >= ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 & q >= ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 ) ) ; then ( |[r,q]| in cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2)) or |[r,q]| in cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)) or |[r,q]| in cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)) or |[r,q]| in cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)) ) by A53, A23, A24, A9, A50, A15, A42, A44, A35, A45, A52, A17, A48, A47, A30, A33, A55, A56, A57, A58; hence x in (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) by A54, Lm3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) or x in cell ((Gauge (D,i)),m,n) ) A59: (2 * m) - 3 < (2 * m) - 2 by XREAL_1:15; (E-bound D) - (W-bound D) >= 0 by SPRECT_1:21, XREAL_1:48; then (((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 3) <= (((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 2) by A59, XREAL_1:64; then A60: (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 3)) <= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * ((2 * m) - 2)) by XREAL_1:6; assume A61: x in (((cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)))) \/ (cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1))) ; ::_thesis: x in cell ((Gauge (D,i)),m,n) percases ( x in cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2)) or x in cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)) or x in cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)) or x in cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)) ) by A61, Lm3; suppose x in cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 2)) ; ::_thesis: x in cell ((Gauge (D,i)),m,n) then consider r, q being Real such that A62: x = |[r,q]| and A63: ((Gauge (D,(i + 1))) * (((2 * m) -' 2),1)) `1 <= r and A64: r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 2) + 1),1)) `1 and A65: ((Gauge (D,(i + 1))) * (1,((2 * n) -' 2))) `2 <= q and A66: q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 2) + 1))) `2 by A42; A67: q <= ((Gauge (D,i)) * (1,(n + 1))) `2 by A38, A9, A7, A40, A47, A66, XXREAL_0:2; r <= ((Gauge (D,i)) * ((m + 1),1)) `1 by A19, A24, A60, A27, A48, A64, XXREAL_0:2; hence x in cell ((Gauge (D,i)),m,n) by A46, A30, A33, A62, A63, A65, A67; ::_thesis: verum end; suppose x in cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 2)) ; ::_thesis: x in cell ((Gauge (D,i)),m,n) then consider r, q being Real such that A68: x = |[r,q]| and A69: ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 <= r and A70: r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 1) + 1),1)) `1 and A71: ((Gauge (D,(i + 1))) * (1,((2 * n) -' 2))) `2 <= q and A72: q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 2) + 1))) `2 by A44; A73: ((Gauge (D,i)) * (m,1)) `1 <= r by A30, A36, A69, XXREAL_0:2; q <= ((Gauge (D,i)) * (1,(n + 1))) `2 by A38, A9, A7, A40, A47, A72, XXREAL_0:2; hence x in cell ((Gauge (D,i)),m,n) by A24, A50, A46, A52, A48, A33, A68, A70, A71, A73; ::_thesis: verum end; suppose x in cell ((Gauge (D,(i + 1))),((2 * m) -' 2),((2 * n) -' 1)) ; ::_thesis: x in cell ((Gauge (D,i)),m,n) then consider r, q being Real such that A74: x = |[r,q]| and A75: ((Gauge (D,(i + 1))) * (((2 * m) -' 2),1)) `1 <= r and A76: r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 2) + 1),1)) `1 and A77: ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 <= q and A78: q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 1) + 1))) `2 by A35; A79: ((Gauge (D,i)) * (1,n)) `2 <= q by A33, A49, A77, XXREAL_0:2; r <= ((Gauge (D,i)) * ((m + 1),1)) `1 by A19, A24, A60, A27, A48, A76, XXREAL_0:2; hence x in cell ((Gauge (D,i)),m,n) by A9, A15, A46, A17, A47, A30, A74, A75, A78, A79; ::_thesis: verum end; suppose x in cell ((Gauge (D,(i + 1))),((2 * m) -' 1),((2 * n) -' 1)) ; ::_thesis: x in cell ((Gauge (D,i)),m,n) then consider r, q being Real such that A80: x = |[r,q]| and A81: ((Gauge (D,(i + 1))) * (((2 * m) -' 1),1)) `1 <= r and A82: r <= ((Gauge (D,(i + 1))) * ((((2 * m) -' 1) + 1),1)) `1 and A83: ((Gauge (D,(i + 1))) * (1,((2 * n) -' 1))) `2 <= q and A84: q <= ((Gauge (D,(i + 1))) * (1,(((2 * n) -' 1) + 1))) `2 by A45; A85: ((Gauge (D,i)) * (1,n)) `2 <= q by A33, A49, A83, XXREAL_0:2; ((Gauge (D,i)) * (m,1)) `1 <= r by A30, A36, A81, XXREAL_0:2; hence x in cell ((Gauge (D,i)),m,n) by A24, A9, A50, A15, A46, A52, A17, A48, A47, A80, A82, A84, A85; ::_thesis: verum end; end; end; theorem :: JORDAN1D:6 for m, i, n being Element of NAT for D being compact non horizontal non vertical Subset of (TOP-REAL 2) for k being Element of NAT st 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) holds cell ((Gauge (D,i)),m,n) = union { (cell ((Gauge (D,(i + k))),a,b)) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) } proof let m, i, n be Element of NAT ; ::_thesis: for D being compact non horizontal non vertical Subset of (TOP-REAL 2) for k being Element of NAT st 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) holds cell ((Gauge (D,i)),m,n) = union { (cell ((Gauge (D,(i + k))),a,b)) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) } let D be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for k being Element of NAT st 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) holds cell ((Gauge (D,i)),m,n) = union { (cell ((Gauge (D,(i + k))),a,b)) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) } let k be Element of NAT ; ::_thesis: ( 2 <= m & m + 1 < len (Gauge (D,i)) & 2 <= n & n + 1 < len (Gauge (D,i)) implies cell ((Gauge (D,i)),m,n) = union { (cell ((Gauge (D,(i + k))),a,b)) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) } ) assume that A1: 2 <= m and A2: m + 1 < len (Gauge (D,i)) and A3: 2 <= n and A4: n + 1 < len (Gauge (D,i)) ; ::_thesis: cell ((Gauge (D,i)),m,n) = union { (cell ((Gauge (D,(i + k))),a,b)) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) } deffunc H1( Element of NAT ) -> set = { (cell ((Gauge (D,(i + $1))),a,b)) where a, b is Element of NAT : ( (((2 |^ $1) * m) - (2 |^ ($1 + 1))) + 2 <= a & a <= (((2 |^ $1) * m) - (2 |^ $1)) + 1 & (((2 |^ $1) * n) - (2 |^ ($1 + 1))) + 2 <= b & b <= (((2 |^ $1) * n) - (2 |^ $1)) + 1 ) } ; defpred S1[ Element of NAT ] means cell ((Gauge (D,i)),m,n) = union H1($1); A5: for w being Element of NAT st S1[w] holds S1[w + 1] proof let w be Element of NAT ; ::_thesis: ( S1[w] implies S1[w + 1] ) assume A6: S1[w] ; ::_thesis: S1[w + 1] A7: len (Gauge (D,(i + w))) = (2 |^ (i + w)) + 3 by JORDAN8:def_1; A8: (i + w) + 1 = i + (w + 1) ; H1(w + 1) is_finer_than H1(w) proof A9: now__::_thesis:_for_a_being_odd_Element_of_NAT_holds_2_*_((a_div_2)_+_1)_=_a_+_1 let a be odd Element of NAT ; ::_thesis: 2 * ((a div 2) + 1) = a + 1 consider e being Element of NAT such that A10: a = (2 * e) + 1 by ABIAN:9; A11: (2 * e) mod 2 = 0 by NAT_D:13; thus 2 * ((a div 2) + 1) = (2 * (a div 2)) + (2 * 1) .= (2 * (((2 * e) div 2) + (1 div 2))) + 2 by A10, A11, NAT_D:19 .= (2 * (e + 0)) + (1 + 1) by Lm1, NAT_D:20 .= a + 1 by A10 ; ::_thesis: verum end; A12: now__::_thesis:_for_m_being_Element_of_NAT_holds_2_*_((((2_|^_w)_*_m)_-_(2_|^_w))_+_1)_=_((((2_|^_(w_+_1))_*_m)_-_(2_|^_(w_+_1)))_+_1)_+_1 let m be Element of NAT ; ::_thesis: 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 thus 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((2 * ((2 |^ w) * m)) - (2 * (2 |^ w))) + (1 + 1) .= (((2 * (2 |^ w)) * m) - (2 |^ (w + 1))) + (1 + 1) by NEWTON:6 .= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + (1 + 1) by NEWTON:6 .= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 ; ::_thesis: verum end; A13: now__::_thesis:_for_m_being_Element_of_NAT_ for_a_being_odd_Element_of_NAT_st_a_<=_(((2_|^_(w_+_1))_*_m)_-_(2_|^_(w_+_1)))_+_1_holds_ (a_div_2)_+_1_<=_(((2_|^_w)_*_m)_-_(2_|^_w))_+_1 let m be Element of NAT ; ::_thesis: for a being odd Element of NAT st a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 holds (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 let a be odd Element of NAT ; ::_thesis: ( a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 implies (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 ) assume a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 ; ::_thesis: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 then A14: a + 1 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by XREAL_1:6; 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by A12; then 2 * ((a div 2) + 1) <= 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) by A9, A14; hence (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by XREAL_1:68; ::_thesis: verum end; A15: now__::_thesis:_for_a_being_even_Element_of_NAT_holds_2_*_((a_div_2)_+_1)_=_a_+_2 let a be even Element of NAT ; ::_thesis: 2 * ((a div 2) + 1) = a + 2 A16: ex e being Element of NAT st a = 2 * e by ABIAN:def_2; thus 2 * ((a div 2) + 1) = (2 * (a div 2)) + (2 * 1) .= a + 2 by A16, NAT_D:20 ; ::_thesis: verum end; A17: now__::_thesis:_for_m_being_Element_of_NAT_ for_a_being_even_Element_of_NAT_st_a_<=_(((2_|^_(w_+_1))_*_m)_-_(2_|^_(w_+_1)))_+_1_holds_ (a_div_2)_+_1_<=_(((2_|^_w)_*_m)_-_(2_|^_w))_+_1 let m be Element of NAT ; ::_thesis: for a being even Element of NAT st a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 holds (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 let a be even Element of NAT ; ::_thesis: ( a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 implies (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 ) assume a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 ; ::_thesis: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 then a < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by XXREAL_0:1; then a + 1 <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by INT_1:7; then (a + 1) + 1 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by XREAL_1:6; then A18: a + (1 + 1) <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 ; 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) = ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 1 by A12; then 2 * ((a div 2) + 1) <= 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) by A15, A18; hence (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by XREAL_1:68; ::_thesis: verum end; let X be set ; :: according to SETFAM_1:def_2 ::_thesis: ( not X in H1(w + 1) or ex b1 being set st ( b1 in H1(w) & X c= b1 ) ) assume X in H1(w + 1) ; ::_thesis: ex b1 being set st ( b1 in H1(w) & X c= b1 ) then consider a, b being Element of NAT such that A19: X = cell ((Gauge (D,(i + (w + 1)))),a,b) and A20: (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a and A21: a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 and A22: (((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2 <= b and A23: b <= (((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1 ; take Y = cell ((Gauge (D,(i + w))),((a div 2) + 1),((b div 2) + 1)); ::_thesis: ( Y in H1(w) & X c= Y ) deffunc H2( Element of NAT , Element of NAT ) -> Element of K10( the U1 of (TOP-REAL 2)) = cell ((Gauge (D,((i + w) + 1))),((2 * ((a div 2) + 1)) -' $1),((2 * ((b div 2) + 1)) -' $2)); A24: now__::_thesis:_for_a,_m_being_Element_of_NAT_st_2_<=_m_holds_ 0_+_2_<=_(((2_|^_(w_+_1))_*_m)_-_(2_|^_((w_+_1)_+_1)))_+_2 let a, m be Element of NAT ; ::_thesis: ( 2 <= m implies 0 + 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 ) A25: 2 |^ ((w + 1) + 1) = (2 |^ (w + 1)) * (2 |^ 1) by NEWTON:8 .= (2 |^ (w + 1)) * 2 by NEWTON:5 ; assume 2 <= m ; ::_thesis: 0 + 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 then (2 |^ (w + 1)) * m >= 2 |^ ((w + 1) + 1) by A25, XREAL_1:64; then 0 <= ((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1)) by XREAL_1:48; hence 0 + 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 by XREAL_1:6; ::_thesis: verum end; then 2 <= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 by A1; then 2 <= a by A20, XXREAL_0:2; then 2 div 2 <= a div 2 by NAT_2:24; then A26: 1 + 1 <= (a div 2) + 1 by Lm2, XREAL_1:6; A27: now__::_thesis:_for_a,_m_being_Element_of_NAT_st_m_+_1_<_len_(Gauge_(D,i))_&_a_<=_(((2_|^_(w_+_1))_*_m)_-_(2_|^_(w_+_1)))_+_1_holds_ ((a_div_2)_+_1)_+_1_<_len_(Gauge_(D,(i_+_w))) let a, m be Element of NAT ; ::_thesis: ( m + 1 < len (Gauge (D,i)) & a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 implies ((a div 2) + 1) + 1 < len (Gauge (D,(i + w))) ) assume m + 1 < len (Gauge (D,i)) ; ::_thesis: ( a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 implies ((a div 2) + 1) + 1 < len (Gauge (D,(i + w))) ) then m + 1 < (2 |^ i) + 3 by JORDAN8:def_1; then (2 * (m + 1)) -' 2 < (2 |^ (i + 1)) + 3 by Lm13; then ((2 * m) + (2 * 1)) -' 2 < (2 |^ (i + 1)) + 3 ; then 2 * m < (2 |^ (i + 1)) + 3 by NAT_D:34; then (1 / 2) * (2 * m) < (1 / 2) * ((2 |^ (i + 1)) + 3) by XREAL_1:68; then m < ((1 / 2) * (2 |^ (i + 1))) + ((1 / 2) * 3) ; then A28: m < (2 |^ i) + ((1 / 2) * 3) by Th2; (2 |^ i) + (3 / 2) < (2 |^ i) + 2 by XREAL_1:6; then m < (2 |^ i) + 2 by A28, XXREAL_0:2; then m + 1 <= (2 |^ i) + 2 by NAT_1:13; then (m + 1) - 2 <= ((2 |^ i) + 2) - 2 by XREAL_1:9; then (2 |^ (w + 1)) * (m - 1) <= (2 |^ (w + 1)) * (2 |^ i) by XREAL_1:64; then ((2 |^ (w + 1)) * (m - 1)) + 5 < ((2 |^ (w + 1)) * (2 |^ i)) + 6 by XREAL_1:8; then A29: ((2 |^ (w + 1)) * (m - 1)) + 5 < (2 |^ ((w + 1) + i)) + 6 by NEWTON:8; then A30: (((2 |^ (w + 1)) * (m - 1)) + 1) + (3 + 1) < (2 * (2 |^ (i + w))) + 6 by A8, NEWTON:6; A31: ((((2 |^ (w + 1)) * (m - 1)) + 1) + 3) + 1 < (2 * (2 |^ (i + w))) + (2 * 3) by A8, A29, NEWTON:6; assume a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 ; ::_thesis: ((a div 2) + 1) + 1 < len (Gauge (D,(i + w))) then a + 3 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3 by XREAL_1:6; then A32: (a + 3) + 0 < (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3) + 1 by XREAL_1:8; then A33: (a + 3) + 1 <= (((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1) + 3) + 1 by INT_1:7; now__::_thesis:_2_*_(((a_div_2)_+_1)_+_1)_<_2_*_((2_|^_(i_+_w))_+_3) percases ( a is odd or a is even ) ; supposeA34: a is odd ; ::_thesis: 2 * (((a div 2) + 1) + 1) < 2 * ((2 |^ (i + w)) + 3) 2 * (((a div 2) + 1) + 1) = (2 * ((a div 2) + 1)) + (2 * 1) .= (a + 1) + 2 by A9, A34 .= a + (1 + 2) ; hence 2 * (((a div 2) + 1) + 1) < 2 * ((2 |^ (i + w)) + 3) by A32, A30, XXREAL_0:2; ::_thesis: verum end; supposeA35: a is even ; ::_thesis: 2 * (((a div 2) + 1) + 1) < 2 * ((2 |^ (i + w)) + 3) 2 * (((a div 2) + 1) + 1) = (2 * ((a div 2) + 1)) + (2 * 1) .= (a + 2) + 2 by A15, A35 .= a + (2 + 2) ; hence 2 * (((a div 2) + 1) + 1) < 2 * ((2 |^ (i + w)) + 3) by A33, A31, XXREAL_0:2; ::_thesis: verum end; end; end; hence ((a div 2) + 1) + 1 < len (Gauge (D,(i + w))) by A7, XREAL_1:64; ::_thesis: verum end; then A36: ((b div 2) + 1) + 1 < len (Gauge (D,(i + w))) by A4, A23; 2 <= (((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2 by A3, A24; then 2 <= b by A22, XXREAL_0:2; then 2 div 2 <= b div 2 by NAT_2:24; then A37: 1 + 1 <= (b div 2) + 1 by Lm2, XREAL_1:6; ((a div 2) + 1) + 1 < len (Gauge (D,(i + w))) by A2, A21, A27; then A38: Y = ((H2(2,2) \/ H2(1,2)) \/ H2(2,1)) \/ H2(1,1) by A26, A37, A36, Th5; A39: now__::_thesis:_for_m_being_Element_of_NAT_holds_2_*_((((2_|^_w)_*_m)_-_(2_|^_(w_+_1)))_+_2)_=_((((2_|^_(w_+_1))_*_m)_-_(2_|^_((w_+_1)_+_1)))_+_2)_+_2 let m be Element of NAT ; ::_thesis: 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 thus 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((2 * ((2 |^ w) * m)) - (2 * (2 |^ (w + 1)))) + (2 + 2) .= (((2 * (2 |^ w)) * m) - (2 |^ ((w + 1) + 1))) + (2 + 2) by NEWTON:6 .= (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (2 + 2) by NEWTON:6 .= ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 ; ::_thesis: verum end; A40: now__::_thesis:_for_m_being_Element_of_NAT_ for_a_being_even_Element_of_NAT_st_(((2_|^_(w_+_1))_*_m)_-_(2_|^_((w_+_1)_+_1)))_+_2_<=_a_holds_ (((2_|^_w)_*_m)_-_(2_|^_(w_+_1)))_+_2_<=_(a_div_2)_+_1 let m be Element of NAT ; ::_thesis: for a being even Element of NAT st (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a holds (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 let a be even Element of NAT ; ::_thesis: ( (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a implies (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 ) assume (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a ; ::_thesis: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 then A41: ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 <= a + 2 by XREAL_1:6; 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 by A39; then 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= 2 * ((a div 2) + 1) by A15, A41; hence (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by XREAL_1:68; ::_thesis: verum end; A42: now__::_thesis:_for_m_being_Element_of_NAT_ for_a_being_odd_Element_of_NAT_st_(((2_|^_(w_+_1))_*_m)_-_(2_|^_((w_+_1)_+_1)))_+_2_<=_a_holds_ (((2_|^_w)_*_m)_-_(2_|^_(w_+_1)))_+_2_<=_(a_div_2)_+_1 let m be Element of NAT ; ::_thesis: for a being odd Element of NAT st (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a holds (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 let a be odd Element of NAT ; ::_thesis: ( (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a implies (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 ) assume (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= a ; ::_thesis: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 then (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 < a by XXREAL_0:1; then ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 1 < a + 1 by XREAL_1:6; then A43: (((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 1) + 1 <= a + 1 by INT_1:7; 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) = ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2) + 2 by A39; then 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= 2 * ((a div 2) + 1) by A9, A43; hence (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by XREAL_1:68; ::_thesis: verum end; percases ( ( a is odd & b is odd ) or ( a is odd & b is even ) or ( a is even & b is odd ) or ( a is even & b is even ) ) ; supposeA44: ( a is odd & b is odd ) ; ::_thesis: ( Y in H1(w) & X c= Y ) then A45: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= (b div 2) + 1 by A22, A42; A46: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by A21, A13, A44; A47: (b div 2) + 1 <= (((2 |^ w) * n) - (2 |^ w)) + 1 by A23, A13, A44; (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by A20, A42, A44; hence Y in H1(w) by A46, A45, A47; ::_thesis: X c= Y A48: (2 * ((b div 2) + 1)) -' 1 = (b + 1) -' 1 by A9, A44 .= b by NAT_D:34 ; (2 * ((a div 2) + 1)) -' 1 = (a + 1) -' 1 by A9, A44 .= a by NAT_D:34 ; hence X c= Y by A19, A38, A48, XBOOLE_1:7; ::_thesis: verum end; supposeA49: ( a is odd & b is even ) ; ::_thesis: ( Y in H1(w) & X c= Y ) then A50: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= (b div 2) + 1 by A22, A40; A51: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by A21, A13, A49; A52: (b div 2) + 1 <= (((2 |^ w) * n) - (2 |^ w)) + 1 by A23, A17, A49; (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by A20, A42, A49; hence Y in H1(w) by A51, A50, A52; ::_thesis: X c= Y A53: H2(2,2) \/ H2(1,2) c= (H2(2,2) \/ H2(1,2)) \/ H2(2,1) by XBOOLE_1:7; H2(1,2) c= H2(2,2) \/ H2(1,2) by XBOOLE_1:7; then A54: H2(1,2) c= (H2(2,2) \/ H2(1,2)) \/ H2(2,1) by A53, XBOOLE_1:1; A55: (H2(2,2) \/ H2(1,2)) \/ H2(2,1) c= Y by A38, XBOOLE_1:7; A56: (2 * ((b div 2) + 1)) -' 2 = (b + 2) -' 2 by A15, A49 .= b by NAT_D:34 ; (2 * ((a div 2) + 1)) -' 1 = (a + 1) -' 1 by A9, A49 .= a by NAT_D:34 ; hence X c= Y by A19, A56, A54, A55, XBOOLE_1:1; ::_thesis: verum end; supposeA57: ( a is even & b is odd ) ; ::_thesis: ( Y in H1(w) & X c= Y ) then A58: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= (b div 2) + 1 by A22, A42; A59: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by A21, A17, A57; A60: (b div 2) + 1 <= (((2 |^ w) * n) - (2 |^ w)) + 1 by A23, A13, A57; (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by A20, A40, A57; hence Y in H1(w) by A59, A58, A60; ::_thesis: X c= Y A61: H2(2,1) c= (H2(2,2) \/ H2(1,2)) \/ H2(2,1) by XBOOLE_1:7; A62: (H2(2,2) \/ H2(1,2)) \/ H2(2,1) c= Y by A38, XBOOLE_1:7; A63: (2 * ((b div 2) + 1)) -' 1 = (b + 1) -' 1 by A9, A57 .= b by NAT_D:34 ; (2 * ((a div 2) + 1)) -' 2 = (a + 2) -' 2 by A15, A57 .= a by NAT_D:34 ; hence X c= Y by A19, A63, A61, A62, XBOOLE_1:1; ::_thesis: verum end; supposeA64: ( a is even & b is even ) ; ::_thesis: ( Y in H1(w) & X c= Y ) then A65: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= (b div 2) + 1 by A22, A40; A66: (a div 2) + 1 <= (((2 |^ w) * m) - (2 |^ w)) + 1 by A21, A17, A64; A67: (b div 2) + 1 <= (((2 |^ w) * n) - (2 |^ w)) + 1 by A23, A17, A64; (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= (a div 2) + 1 by A20, A40, A64; hence Y in H1(w) by A66, A65, A67; ::_thesis: X c= Y A68: (2 * ((b div 2) + 1)) -' 2 = (b + 2) -' 2 by A15, A64 .= b by NAT_D:34 ; (2 * ((a div 2) + 1)) -' 2 = (a + 2) -' 2 by A15, A64 .= a by NAT_D:34 ; then X c= H2(2,2) \/ ((H2(1,2) \/ H2(2,1)) \/ H2(1,1)) by A19, A68, XBOOLE_1:7; then X c= (H2(2,2) \/ (H2(1,2) \/ H2(2,1))) \/ H2(1,1) by XBOOLE_1:4; hence X c= Y by A38, XBOOLE_1:4; ::_thesis: verum end; end; end; then A69: union H1(w + 1) c= union H1(w) by SETFAM_1:13; A70: len (Gauge (D,i)) = (2 |^ i) + 3 by JORDAN8:def_1; for x being set st x in H1(w) holds ex K being set st ( K c= H1(w + 1) & x c= union K ) proof let x be set ; ::_thesis: ( x in H1(w) implies ex K being set st ( K c= H1(w + 1) & x c= union K ) ) assume x in H1(w) ; ::_thesis: ex K being set st ( K c= H1(w + 1) & x c= union K ) then consider a, b being Element of NAT such that A71: x = cell ((Gauge (D,(i + w))),a,b) and A72: (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= a and A73: a <= (((2 |^ w) * m) - (2 |^ w)) + 1 and A74: (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 <= b and A75: b <= (((2 |^ w) * n) - (2 |^ w)) + 1 ; take K = {(cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 2),((2 * b) -' 2))),(cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 1),((2 * b) -' 2))),(cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 2),((2 * b) -' 1))),(cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 1),((2 * b) -' 1)))}; ::_thesis: ( K c= H1(w + 1) & x c= union K ) A76: now__::_thesis:_for_m_being_Element_of_NAT_st_2_<=_m_holds_ 0_+_2_<=_(((2_|^_w)_*_m)_-_(2_|^_(w_+_1)))_+_2 let m be Element of NAT ; ::_thesis: ( 2 <= m implies 0 + 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 ) assume 2 <= m ; ::_thesis: 0 + 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 then (2 |^ w) * m >= (2 |^ w) * 2 by XREAL_1:64; then (2 |^ w) * m >= 2 |^ (w + 1) by NEWTON:6; then 0 <= ((2 |^ w) * m) - (2 |^ (w + 1)) by XREAL_1:48; hence 0 + 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 by XREAL_1:6; ::_thesis: verum end; then A77: 2 <= (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 by A1; then A78: 2 <= a by A72, XXREAL_0:2; A79: (2 * a) -' 2 = (2 * a) - 2 by A72, A77, Lm7, XXREAL_0:2; A80: 2 <= (((2 |^ w) * n) - (2 |^ (w + 1))) + 2 by A3, A76; then A81: 2 <= b by A74, XXREAL_0:2; A82: (2 * b) -' 2 = (2 * b) - 2 by A74, A80, Lm7, XXREAL_0:2; (2 * b) -' 1 = (2 * b) - 1 by A81, Lm8, XXREAL_0:2; then A83: (2 * b) -' 2 < (2 * b) -' 1 by A82, XREAL_1:15; (2 * a) -' 1 = (2 * a) - 1 by A78, Lm8, XXREAL_0:2; then A84: (2 * a) -' 2 < (2 * a) -' 1 by A79, XREAL_1:15; hereby :: according to TARSKI:def_3 ::_thesis: x c= union K A85: now__::_thesis:_for_a,_m_being_Element_of_NAT_st_2_<=_a_&_a_<=_(((2_|^_w)_*_m)_-_(2_|^_w))_+_1_holds_ (2_*_a)_-'_2_<_(((2_|^_(w_+_1))_*_m)_-_(2_|^_(w_+_1)))_+_1 let a, m be Element of NAT ; ::_thesis: ( 2 <= a & a <= (((2 |^ w) * m) - (2 |^ w)) + 1 implies (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 ) assume A86: 2 <= a ; ::_thesis: ( a <= (((2 |^ w) * m) - (2 |^ w)) + 1 implies (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 ) assume a <= (((2 |^ w) * m) - (2 |^ w)) + 1 ; ::_thesis: (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 then 2 * a <= 2 * ((((2 |^ w) * m) - (2 |^ w)) + 1) by XREAL_1:64; then 2 * a <= (((2 * (2 |^ w)) * m) - (2 * (2 |^ w))) + 2 ; then 2 * a <= (((2 |^ (w + 1)) * m) - (2 * (2 |^ w))) + 2 by NEWTON:6; then 2 * a <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2 by NEWTON:6; then (2 * a) - 2 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2) - 2 by XREAL_1:9; then A87: (2 * a) -' 2 <= ((((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 2) - 2 by A86, Lm7; (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 0 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by XREAL_1:6; hence (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by A87, XXREAL_0:2; ::_thesis: verum end; then A88: (2 * a) -' 2 < (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by A73, A78; then ((2 * a) -' 2) + 1 <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by INT_1:7; then A89: (2 * a) -' 1 <= (((2 |^ (w + 1)) * m) - (2 |^ (w + 1))) + 1 by A78, Lm9, XXREAL_0:2; A90: now__::_thesis:_for_a,_m_being_Element_of_NAT_st_2_<=_a_&_(((2_|^_w)_*_m)_-_(2_|^_(w_+_1)))_+_2_<=_a_holds_ (((2_|^_(w_+_1))_*_m)_-_(2_|^_((w_+_1)_+_1)))_+_(4_-_2)_<=_(2_*_a)_-'_2 let a, m be Element of NAT ; ::_thesis: ( 2 <= a & (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= a implies (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2) <= (2 * a) -' 2 ) assume A91: 2 <= a ; ::_thesis: ( (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= a implies (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2) <= (2 * a) -' 2 ) assume (((2 |^ w) * m) - (2 |^ (w + 1))) + 2 <= a ; ::_thesis: (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2) <= (2 * a) -' 2 then 2 * ((((2 |^ w) * m) - (2 |^ (w + 1))) + 2) <= 2 * a by XREAL_1:64; then (((2 * (2 |^ w)) * m) - (2 * (2 |^ (w + 1)))) + 4 <= 2 * a ; then (((2 |^ (w + 1)) * m) - (2 * (2 |^ (w + 1)))) + 4 <= 2 * a by NEWTON:6; then (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 4 <= 2 * a by NEWTON:6; then ((((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 4) - 2 <= (2 * a) - 2 by XREAL_1:9; hence (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + (4 - 2) <= (2 * a) -' 2 by A91, Lm7; ::_thesis: verum end; then A92: (((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2 <= (2 * b) -' 2 by A74, A81; then A93: (((2 |^ (w + 1)) * n) - (2 |^ ((w + 1) + 1))) + 2 <= (2 * b) -' 1 by A83, XXREAL_0:2; let q be set ; ::_thesis: ( q in K implies q in H1(w + 1) ) assume q in K ; ::_thesis: q in H1(w + 1) then A94: ( q = cell ((Gauge (D,(i + (w + 1)))),((2 * a) -' 2),((2 * b) -' 2)) or q = cell ((Gauge (D,(i + (w + 1)))),((2 * a) -' 1),((2 * b) -' 2)) or q = cell ((Gauge (D,(i + (w + 1)))),((2 * a) -' 2),((2 * b) -' 1)) or q = cell ((Gauge (D,(i + (w + 1)))),((2 * a) -' 1),((2 * b) -' 1)) ) by ENUMSET1:def_2; A95: (2 * b) -' 2 < (((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1 by A75, A81, A85; then ((2 * b) -' 2) + 1 <= (((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1 by INT_1:7; then A96: (2 * b) -' 1 <= (((2 |^ (w + 1)) * n) - (2 |^ (w + 1))) + 1 by A81, Lm9, XXREAL_0:2; A97: (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= (2 * a) -' 2 by A72, A78, A90; then (((2 |^ (w + 1)) * m) - (2 |^ ((w + 1) + 1))) + 2 <= (2 * a) -' 1 by A84, XXREAL_0:2; hence q in H1(w + 1) by A97, A88, A89, A92, A95, A96, A93, A94; ::_thesis: verum end; A98: now__::_thesis:_for_a,_m_being_Element_of_NAT_st_m_+_1_<_len_(Gauge_(D,i))_&_a_<=_(((2_|^_w)_*_m)_-_(2_|^_w))_+_1_holds_ a_+_1_<_len_(Gauge_(D,(i_+_w))) let a, m be Element of NAT ; ::_thesis: ( m + 1 < len (Gauge (D,i)) & a <= (((2 |^ w) * m) - (2 |^ w)) + 1 implies a + 1 < len (Gauge (D,(i + w))) ) assume m + 1 < len (Gauge (D,i)) ; ::_thesis: ( a <= (((2 |^ w) * m) - (2 |^ w)) + 1 implies a + 1 < len (Gauge (D,(i + w))) ) then (m + 1) - 2 < ((2 |^ i) + 3) - 2 by A70, XREAL_1:9; then m - 1 < (2 |^ i) + (3 - 2) ; then m - 1 <= (2 |^ i) + 0 by INT_1:7; then (2 |^ w) * (m - 1) <= (2 |^ w) * (2 |^ i) by XREAL_1:64; then (2 |^ w) * (m - 1) <= 2 |^ (w + i) by NEWTON:8; then A99: ((2 |^ w) * (m - 1)) + 3 <= (2 |^ (w + i)) + 3 by XREAL_1:6; assume a <= (((2 |^ w) * m) - (2 |^ w)) + 1 ; ::_thesis: a + 1 < len (Gauge (D,(i + w))) then a + 1 <= ((((2 |^ w) * m) - (2 |^ w)) + 1) + 1 by XREAL_1:6; then a + 1 < (((((2 |^ w) * m) - (2 |^ w)) + 1) + 1) + 1 by XREAL_1:145; hence a + 1 < len (Gauge (D,(i + w))) by A7, A99, XXREAL_0:2; ::_thesis: verum end; then A100: b + 1 < len (Gauge (D,(i + w))) by A4, A75; a + 1 < len (Gauge (D,(i + w))) by A2, A73, A98; then cell ((Gauge (D,(i + w))),a,b) = (((cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 2),((2 * b) -' 2))) \/ (cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 1),((2 * b) -' 2)))) \/ (cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 2),((2 * b) -' 1)))) \/ (cell ((Gauge (D,((i + w) + 1))),((2 * a) -' 1),((2 * b) -' 1))) by A78, A81, A100, Th5; hence x c= union K by A71, Lm4; ::_thesis: verum end; hence cell ((Gauge (D,i)),m,n) c= union H1(w + 1) by A6, Th1; :: according to XBOOLE_0:def_10 ::_thesis: union H1(w + 1) c= cell ((Gauge (D,i)),m,n) let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in union H1(w + 1) or d in cell ((Gauge (D,i)),m,n) ) assume d in union H1(w + 1) ; ::_thesis: d in cell ((Gauge (D,i)),m,n) hence d in cell ((Gauge (D,i)),m,n) by A6, A69; ::_thesis: verum end; A101: now__::_thesis:_for_m_being_Element_of_NAT_holds_ (_(((2_|^_0)_*_m)_-_(2_|^_(0_+_1)))_+_2_=_m_&_(((2_|^_0)_*_m)_-_(2_|^_0))_+_1_=_m_) let m be Element of NAT ; ::_thesis: ( (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 = m & (((2 |^ 0) * m) - (2 |^ 0)) + 1 = m ) A102: (2 |^ 0) * m = 1 * m by NEWTON:4; hence (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 = (m - 2) + 2 by NEWTON:5 .= m ; ::_thesis: (((2 |^ 0) * m) - (2 |^ 0)) + 1 = m thus (((2 |^ 0) * m) - (2 |^ 0)) + 1 = (m - 1) + 1 by A102, NEWTON:4 .= m ; ::_thesis: verum end; H1( 0 ) = {(cell ((Gauge (D,i)),m,n))} proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(cell ((Gauge (D,i)),m,n))} c= H1( 0 ) let x be set ; ::_thesis: ( x in H1( 0 ) implies x in {(cell ((Gauge (D,i)),m,n))} ) assume x in H1( 0 ) ; ::_thesis: x in {(cell ((Gauge (D,i)),m,n))} then consider a, b being Element of NAT such that A103: x = cell ((Gauge (D,(i + 0))),a,b) and A104: (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 <= a and A105: a <= (((2 |^ 0) * m) - (2 |^ 0)) + 1 and A106: (((2 |^ 0) * n) - (2 |^ (0 + 1))) + 2 <= b and A107: b <= (((2 |^ 0) * n) - (2 |^ 0)) + 1 ; A108: now__::_thesis:_for_a,_m_being_Element_of_NAT_st_(((2_|^_0)_*_m)_-_(2_|^_(0_+_1)))_+_2_<=_a_&_a_<=_(((2_|^_0)_*_m)_-_(2_|^_0))_+_1_holds_ a_=_m let a, m be Element of NAT ; ::_thesis: ( (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 <= a & a <= (((2 |^ 0) * m) - (2 |^ 0)) + 1 implies a = m ) assume that A109: (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 <= a and A110: a <= (((2 |^ 0) * m) - (2 |^ 0)) + 1 ; ::_thesis: a = m A111: (((2 |^ 0) * m) - (2 |^ 0)) + 1 = m by A101; (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 = m by A101; hence a = m by A109, A110, A111, XXREAL_0:1; ::_thesis: verum end; then A112: b = n by A106, A107; a = m by A104, A105, A108; hence x in {(cell ((Gauge (D,i)),m,n))} by A103, A112, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(cell ((Gauge (D,i)),m,n))} or x in H1( 0 ) ) assume x in {(cell ((Gauge (D,i)),m,n))} ; ::_thesis: x in H1( 0 ) then A113: x = cell ((Gauge (D,(i + 0))),m,n) by TARSKI:def_1; A114: m <= (((2 |^ 0) * m) - (2 |^ 0)) + 1 by A101; A115: n <= (((2 |^ 0) * n) - (2 |^ 0)) + 1 by A101; A116: (((2 |^ 0) * n) - (2 |^ (0 + 1))) + 2 <= n by A101; (((2 |^ 0) * m) - (2 |^ (0 + 1))) + 2 <= m by A101; hence x in H1( 0 ) by A113, A114, A116, A115; ::_thesis: verum end; then A117: S1[ 0 ] by ZFMISC_1:25; for w being Element of NAT holds S1[w] from NAT_1:sch_1(A117, A5); hence cell ((Gauge (D,i)),m,n) = union { (cell ((Gauge (D,(i + k))),a,b)) where a, b is Element of NAT : ( (((2 |^ k) * m) - (2 |^ (k + 1))) + 2 <= a & a <= (((2 |^ k) * m) - (2 |^ k)) + 1 & (((2 |^ k) * n) - (2 |^ (k + 1))) + 2 <= b & b <= (((2 |^ k) * n) - (2 |^ k)) + 1 ) } ; ::_thesis: verum end; theorem Th7: :: JORDAN1D:7 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) consider p being Point of (TOP-REAL 2) such that A1: (north_halfline (N-max C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:86, PSCOMP_1:42; A2: p in (north_halfline (N-max C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1; then A3: p in north_halfline (N-max C) by XBOOLE_0:def_4; p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4; then consider i being Element of NAT such that A4: 1 <= i and A5: i + 1 <= len (Cage (C,n)) and A6: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) A7: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A4, A5, TOPREAL1:def_3; A8: len (Gauge (C,n)) >= 4 by JORDAN8:10; then A9: 1 < len (Gauge (C,n)) by XXREAL_0:2; A10: ((len (Gauge (C,n))) -' 1) + 1 = len (Gauge (C,n)) by A8, XREAL_1:235, XXREAL_0:2; then A11: (len (Gauge (C,n))) -' 1 < len (Gauge (C,n)) by NAT_1:13; A12: N-max C = |[((N-max C) `1),((N-max C) `2)]| by EUCLID:53; A13: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:44; A14: (N-max C) `2 = N-bound C by EUCLID:52 .= ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 by A9, JORDAN8:14 ; A15: N-max C in N-most C by PSCOMP_1:42; A16: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; thus A17: ( 1 <= i & i < len (Cage (C,n)) ) by A4, A5, NAT_1:13; ::_thesis: N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) then A18: ((Cage (C,n)) /. i) `2 = p `2 by A3, A6, A15, A7, JORDAN1A:78, SPPOL_1:40; A19: ((Cage (C,n)) /. (i + 1)) `2 = p `2 by A3, A6, A17, A15, A7, JORDAN1A:78, SPPOL_1:40; A20: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i1, j1, i2, j2 being Element of NAT such that A21: [i1,j1] in Indices (Gauge (C,n)) and A22: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and A23: [i2,j2] in Indices (Gauge (C,n)) and A24: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and A25: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A4, A5, JORDAN8:3; A26: 1 <= i1 by A21, MATRIX_1:38; A27: j2 <= width (Gauge (C,n)) by A23, MATRIX_1:38; A28: i1 <= len (Gauge (C,n)) by A21, MATRIX_1:38; A29: 1 <= j1 by A21, MATRIX_1:38; p `2 = N-bound (L~ (Cage (C,n))) by A2, JORDAN1A:82, PSCOMP_1:42; then ((Gauge (C,n)) * (i1,j1)) `2 = ((Gauge (C,n)) * (i1,(len (Gauge (C,n))))) `2 by A22, A18, A26, A28, JORDAN1A:70; then A30: len (Gauge (C,n)) <= j1 by A16, A26, A28, A29, GOBOARD5:4; A31: j1 <= width (Gauge (C,n)) by A21, MATRIX_1:38; then A32: j1 = len (Gauge (C,n)) by A16, A30, XXREAL_0:1; A33: 1 <= j2 by A23, MATRIX_1:38; A34: j1 = j2 proof assume j1 <> j2 ; ::_thesis: contradiction then ( j1 < j2 or j2 < j1 ) by XXREAL_0:1; hence contradiction by A22, A24, A25, A18, A19, A26, A28, A29, A27, A33, A31, GOBOARD5:4; ::_thesis: verum end; A35: 1 <= i2 by A23, MATRIX_1:38; A36: i2 <= len (Gauge (C,n)) by A23, MATRIX_1:38; i1 <= i1 + 1 by NAT_1:11; then A37: ((Cage (C,n)) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1 by A4, A5, A21, A22, A23, A24, A25, A16, A26, A36, A29, A27, A34, A30, JORDAN10:4, JORDAN1A:18; then p `1 <= ((Cage (C,n)) /. (i + 1)) `1 by A6, A7, TOPREAL1:3; then (N-max C) `1 <= ((Gauge (C,n)) * ((i1 + 1),(len (Gauge (C,n))))) `1 by A3, A4, A5, A21, A22, A23, A24, A25, A16, A34, A32, JORDAN10:4, TOPREAL1:def_10; then A38: (N-max C) `1 <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 by A4, A5, A21, A22, A23, A24, A25, A16, A35, A36, A34, A30, A9, GOBOARD5:2, JORDAN10:4; ((Cage (C,n)) /. i) `1 <= p `1 by A6, A7, A37, TOPREAL1:3; then ((Gauge (C,n)) * (i1,(len (Gauge (C,n))))) `1 <= (N-max C) `1 by A3, A22, A32, TOPREAL1:def_10; then A39: ((Gauge (C,n)) * (i1,1)) `1 <= (N-max C) `1 by A16, A26, A28, A9, GOBOARD5:2; len (Gauge (C,n)) >= 1 + 1 by A8, XXREAL_0:2; then A40: (len (Gauge (C,n))) - 1 >= 1 by XREAL_1:19; then (len (Gauge (C,n))) -' 1 >= 1 by XREAL_0:def_2; then ((Gauge (C,n)) * (1,j1)) `2 >= (N-max C) `2 by A16, A32, A9, A14, A13, SPRECT_3:12; then A41: N-max C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j1 -' 1))) `2 <= s & s <= ((Gauge (C,n)) * (1,j1)) `2 ) } by A32, A14, A39, A38, A12; A42: 1 <= i1 by A21, MATRIX_1:38; i1 < len (Gauge (C,n)) by A4, A5, A21, A22, A23, A24, A25, A16, A36, A34, A30, JORDAN10:4, NAT_1:13; then N-max C in cell ((Gauge (C,n)),i1,(j1 -' 1)) by A16, A32, A42, A40, A10, A11, A41, GOBRD11:32; hence N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A4, A5, A20, A21, A22, A23, A24, A25, A16, A34, A30, GOBRD13:24, JORDAN10:4; ::_thesis: verum end; theorem :: JORDAN1D:8 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i) ) A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; consider i being Element of NAT such that A2: 1 <= i and A3: i < len (Cage (C,n)) and A4: N-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th7; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & N-max C in right_cell ((Cage (C,n)),i) ) thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: N-max C in right_cell ((Cage (C,n)),i) i + 1 <= len (Cage (C,n)) by A3, NAT_1:13; then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33; hence N-max C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum end; theorem Th9: :: JORDAN1D:9 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) consider p being Point of (TOP-REAL 2) such that A1: (east_halfline (E-min C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:87, PSCOMP_1:50; A2: p in (east_halfline (E-min C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1; then A3: p in east_halfline (E-min C) by XBOOLE_0:def_4; len (Gauge (C,n)) < (len (Gauge (C,n))) + 1 by NAT_1:13; then A4: (len (Gauge (C,n))) - 1 < len (Gauge (C,n)) by XREAL_1:19; A5: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:44; A6: E-min C = |[((E-min C) `1),((E-min C) `2)]| by EUCLID:53; A7: len (Gauge (C,n)) >= 4 by JORDAN8:10; then A8: 1 < len (Gauge (C,n)) by XXREAL_0:2; A9: ((len (Gauge (C,n))) -' 1) + 1 = len (Gauge (C,n)) by A7, XREAL_1:235, XXREAL_0:2; A10: (E-min C) `1 = E-bound C by EUCLID:52 .= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A8, JORDAN8:12 ; A11: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A12: E-min C in E-most C by PSCOMP_1:50; p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4; then consider i being Element of NAT such that A13: 1 <= i and A14: i + 1 <= len (Cage (C,n)) and A15: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) A16: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A13, A14, TOPREAL1:def_3; thus A17: ( 1 <= i & i < len (Cage (C,n)) ) by A13, A14, NAT_1:13; ::_thesis: E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) then A18: ((Cage (C,n)) /. i) `1 = p `1 by A3, A15, A12, A16, JORDAN1A:79, SPPOL_1:41; A19: ((Cage (C,n)) /. (i + 1)) `1 = p `1 by A3, A15, A17, A12, A16, JORDAN1A:79, SPPOL_1:41; A20: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i1, j1, i2, j2 being Element of NAT such that A21: [i1,j1] in Indices (Gauge (C,n)) and A22: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and A23: [i2,j2] in Indices (Gauge (C,n)) and A24: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and A25: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A13, A14, JORDAN8:3; A26: 1 <= i1 by A21, MATRIX_1:38; A27: j1 <= width (Gauge (C,n)) by A21, MATRIX_1:38; A28: j2 <= width (Gauge (C,n)) by A23, MATRIX_1:38; A29: 1 <= i2 by A23, MATRIX_1:38; A30: 1 <= j1 by A21, MATRIX_1:38; p `1 = E-bound (L~ (Cage (C,n))) by A2, JORDAN1A:83, PSCOMP_1:50; then ((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),j1)) `1 by A22, A18, A11, A30, A27, JORDAN1A:71; then A31: len (Gauge (C,n)) <= i1 by A26, A30, A27, GOBOARD5:3; A32: i1 <= len (Gauge (C,n)) by A21, MATRIX_1:38; then A33: i1 = len (Gauge (C,n)) by A31, XXREAL_0:1; A34: i2 <= len (Gauge (C,n)) by A23, MATRIX_1:38; A35: i1 = i2 proof assume i1 <> i2 ; ::_thesis: contradiction then ( i1 < i2 or i2 < i1 ) by XXREAL_0:1; hence contradiction by A22, A24, A25, A18, A19, A26, A32, A29, A34, A30, A28, GOBOARD5:3; ::_thesis: verum end; then A36: j2 < width (Gauge (C,n)) by A13, A14, A21, A22, A23, A24, A25, A27, A31, JORDAN10:1, NAT_1:13; A37: 1 <= j2 by A23, MATRIX_1:38; j2 <= j2 + 1 by NAT_1:11; then A38: ((Cage (C,n)) /. i) `2 >= ((Cage (C,n)) /. (i + 1)) `2 by A13, A14, A21, A22, A23, A24, A25, A26, A32, A37, A27, A35, A31, JORDAN10:1, JORDAN1A:19; then p `2 <= ((Cage (C,n)) /. i) `2 by A15, A16, TOPREAL1:4; then (E-min C) `2 <= ((Gauge (C,n)) * ((len (Gauge (C,n))),(j2 + 1))) `2 by A3, A13, A14, A21, A22, A23, A24, A25, A35, A33, JORDAN10:1, TOPREAL1:def_11; then A39: (E-min C) `2 <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 by A13, A14, A21, A22, A23, A24, A25, A29, A30, A27, A35, A33, GOBOARD5:1, JORDAN10:1; ((Cage (C,n)) /. (i + 1)) `2 <= p `2 by A15, A16, A38, TOPREAL1:4; then ((Gauge (C,n)) * ((len (Gauge (C,n))),j2)) `2 <= (E-min C) `2 by A3, A24, A35, A33, TOPREAL1:def_11; then A40: ((Gauge (C,n)) * (1,j2)) `2 <= (E-min C) `2 by A29, A28, A37, A35, A33, GOBOARD5:1; len (Gauge (C,n)) >= 1 + 1 by A7, XXREAL_0:2; then A41: (len (Gauge (C,n))) - 1 >= 1 by XREAL_1:19; then (len (Gauge (C,n))) -' 1 >= 1 by XREAL_0:def_2; then ((Gauge (C,n)) * (i1,1)) `1 >= (E-min C) `1 by A11, A33, A8, A10, A5, SPRECT_3:13; then E-min C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 <= r & r <= ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 ) } by A33, A10, A40, A39, A6; then E-min C in cell ((Gauge (C,n)),(i2 -' 1),j2) by A37, A35, A33, A36, A41, A4, A9, GOBRD11:32; hence E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A13, A14, A20, A21, A22, A23, A24, A25, A35, A31, GOBRD13:28, JORDAN10:1; ::_thesis: verum end; theorem :: JORDAN1D:10 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i) ) A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; consider i being Element of NAT such that A2: 1 <= i and A3: i < len (Cage (C,n)) and A4: E-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th9; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & E-min C in right_cell ((Cage (C,n)),i) ) thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: E-min C in right_cell ((Cage (C,n)),i) i + 1 <= len (Cage (C,n)) by A3, NAT_1:13; then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33; hence E-min C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum end; theorem Th11: :: JORDAN1D:11 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) consider p being Point of (TOP-REAL 2) such that A1: (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:87, PSCOMP_1:50; A2: p in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1; then A3: p in east_halfline (E-max C) by XBOOLE_0:def_4; len (Gauge (C,n)) < (len (Gauge (C,n))) + 1 by NAT_1:13; then A4: (len (Gauge (C,n))) - 1 < len (Gauge (C,n)) by XREAL_1:19; A5: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:44; A6: len (Gauge (C,n)) >= 4 by JORDAN8:10; then A7: 1 < len (Gauge (C,n)) by XXREAL_0:2; A8: ((len (Gauge (C,n))) -' 1) + 1 = len (Gauge (C,n)) by A6, XREAL_1:235, XXREAL_0:2; A9: (E-max C) `1 = E-bound C by EUCLID:52 .= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A7, JORDAN8:12 ; A10: E-max C = |[((E-max C) `1),((E-max C) `2)]| by EUCLID:53; A11: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A12: E-max C in E-most C by PSCOMP_1:50; p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4; then consider i being Element of NAT such that A13: 1 <= i and A14: i + 1 <= len (Cage (C,n)) and A15: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) A16: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A13, A14, TOPREAL1:def_3; thus A17: ( 1 <= i & i < len (Cage (C,n)) ) by A13, A14, NAT_1:13; ::_thesis: E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) then A18: ((Cage (C,n)) /. i) `1 = p `1 by A3, A15, A12, A16, JORDAN1A:79, SPPOL_1:41; A19: ((Cage (C,n)) /. (i + 1)) `1 = p `1 by A3, A15, A17, A12, A16, JORDAN1A:79, SPPOL_1:41; A20: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i1, j1, i2, j2 being Element of NAT such that A21: [i1,j1] in Indices (Gauge (C,n)) and A22: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and A23: [i2,j2] in Indices (Gauge (C,n)) and A24: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and A25: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A13, A14, JORDAN8:3; A26: 1 <= i1 by A21, MATRIX_1:38; A27: j1 <= width (Gauge (C,n)) by A21, MATRIX_1:38; A28: i2 <= len (Gauge (C,n)) by A23, MATRIX_1:38; A29: j2 <= width (Gauge (C,n)) by A23, MATRIX_1:38; A30: 1 <= j1 by A21, MATRIX_1:38; p `1 = E-bound (L~ (Cage (C,n))) by A2, JORDAN1A:83, PSCOMP_1:50; then ((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),j1)) `1 by A22, A18, A11, A30, A27, JORDAN1A:71; then A31: len (Gauge (C,n)) <= i1 by A26, A30, A27, GOBOARD5:3; A32: i1 <= len (Gauge (C,n)) by A21, MATRIX_1:38; then A33: i1 = len (Gauge (C,n)) by A31, XXREAL_0:1; A34: 1 <= i2 by A23, MATRIX_1:38; A35: i1 = i2 proof assume i1 <> i2 ; ::_thesis: contradiction then ( i1 < i2 or i2 < i1 ) by XXREAL_0:1; hence contradiction by A22, A24, A25, A18, A19, A26, A32, A34, A28, A30, A29, GOBOARD5:3; ::_thesis: verum end; then A36: j2 < width (Gauge (C,n)) by A13, A14, A21, A22, A23, A24, A25, A27, A31, JORDAN10:1, NAT_1:13; A37: 1 <= j2 by A23, MATRIX_1:38; j2 <= j2 + 1 by NAT_1:11; then A38: ((Cage (C,n)) /. i) `2 >= ((Cage (C,n)) /. (i + 1)) `2 by A13, A14, A21, A22, A23, A24, A25, A26, A32, A37, A27, A35, A31, JORDAN10:1, JORDAN1A:19; then p `2 <= ((Cage (C,n)) /. i) `2 by A15, A16, TOPREAL1:4; then (E-max C) `2 <= ((Gauge (C,n)) * ((len (Gauge (C,n))),(j2 + 1))) `2 by A3, A13, A14, A21, A22, A23, A24, A25, A35, A33, JORDAN10:1, TOPREAL1:def_11; then A39: (E-max C) `2 <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 by A13, A14, A21, A22, A23, A24, A25, A30, A27, A35, A31, A7, GOBOARD5:1, JORDAN10:1; ((Cage (C,n)) /. (i + 1)) `2 <= p `2 by A15, A16, A38, TOPREAL1:4; then ((Gauge (C,n)) * ((len (Gauge (C,n))),j2)) `2 <= (E-max C) `2 by A3, A24, A35, A33, TOPREAL1:def_11; then A40: ((Gauge (C,n)) * (1,j2)) `2 <= (E-max C) `2 by A29, A37, A7, GOBOARD5:1; len (Gauge (C,n)) >= 1 + 1 by A6, XXREAL_0:2; then A41: (len (Gauge (C,n))) - 1 >= 1 by XREAL_1:19; then (len (Gauge (C,n))) -' 1 >= 1 by XREAL_0:def_2; then ((Gauge (C,n)) * (i1,1)) `1 >= (E-max C) `1 by A11, A33, A7, A9, A5, SPRECT_3:13; then E-max C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 <= r & r <= ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 ) } by A33, A9, A40, A39, A10; then E-max C in cell ((Gauge (C,n)),(i2 -' 1),j2) by A37, A35, A33, A36, A41, A4, A8, GOBRD11:32; hence E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A13, A14, A20, A21, A22, A23, A24, A25, A35, A31, GOBRD13:28, JORDAN10:1; ::_thesis: verum end; theorem :: JORDAN1D:12 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i) ) A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; consider i being Element of NAT such that A2: 1 <= i and A3: i < len (Cage (C,n)) and A4: E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th11; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i) ) thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: E-max C in right_cell ((Cage (C,n)),i) i + 1 <= len (Cage (C,n)) by A3, NAT_1:13; then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33; hence E-max C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum end; theorem Th13: :: JORDAN1D:13 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) consider p being Point of (TOP-REAL 2) such that A1: (south_halfline (S-min C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:88, PSCOMP_1:58; A2: p in (south_halfline (S-min C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1; then A3: p in south_halfline (S-min C) by XBOOLE_0:def_4; A4: S-min C = |[((S-min C) `1),((S-min C) `2)]| by EUCLID:53; A5: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A6: len (Gauge (C,n)) >= 4 by JORDAN8:10; then A7: 1 < len (Gauge (C,n)) by XXREAL_0:2; p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4; then consider i being Element of NAT such that A8: 1 <= i and A9: i + 1 <= len (Cage (C,n)) and A10: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) A11: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A8, A9, TOPREAL1:def_3; A12: (S-min C) `2 = S-bound C by EUCLID:52 .= ((Gauge (C,n)) * (1,2)) `2 by A7, JORDAN8:13 ; A13: S-min C in S-most C by PSCOMP_1:58; thus A14: ( 1 <= i & i < len (Cage (C,n)) ) by A8, A9, NAT_1:13; ::_thesis: S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) then A15: ((Cage (C,n)) /. i) `2 = p `2 by A3, A10, A13, A11, JORDAN1A:80, SPPOL_1:40; A16: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i1, j1, i2, j2 being Element of NAT such that A17: [i1,j1] in Indices (Gauge (C,n)) and A18: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and A19: [i2,j2] in Indices (Gauge (C,n)) and A20: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and A21: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A8, A9, JORDAN8:3; A22: 1 <= i1 by A17, MATRIX_1:38; A23: 1 <= j2 by A19, MATRIX_1:38; A24: i2 <= i2 + 1 by NAT_1:11; A25: j2 <= width (Gauge (C,n)) by A19, MATRIX_1:38; A26: i1 <= len (Gauge (C,n)) by A17, MATRIX_1:38; A27: j1 <= width (Gauge (C,n)) by A17, MATRIX_1:38; p `2 = S-bound (L~ (Cage (C,n))) by A2, JORDAN1A:84, PSCOMP_1:58; then ((Gauge (C,n)) * (i1,j1)) `2 = ((Gauge (C,n)) * (i1,1)) `2 by A18, A15, A22, A26, JORDAN1A:72; then A28: 1 >= j1 by A22, A26, A27, GOBOARD5:4; A29: 1 <= j1 by A17, MATRIX_1:38; then A30: j1 = 1 by A28, XXREAL_0:1; A31: ((Cage (C,n)) /. (i + 1)) `2 = p `2 by A3, A10, A14, A13, A11, JORDAN1A:80, SPPOL_1:40; A32: j1 = j2 proof assume j1 <> j2 ; ::_thesis: contradiction then ( j1 < j2 or j2 < j1 ) by XXREAL_0:1; hence contradiction by A18, A20, A21, A15, A31, A22, A26, A29, A25, A23, A27, GOBOARD5:4; ::_thesis: verum end; then A33: i2 < len (Gauge (C,n)) by A8, A9, A17, A18, A19, A20, A21, A26, A28, JORDAN10:3, NAT_1:13; 1 <= i2 by A19, MATRIX_1:38; then A34: ((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1 by A8, A9, A17, A18, A19, A20, A21, A26, A29, A25, A23, A27, A28, A24, JORDAN10:3, JORDAN1A:18; then p `1 <= ((Cage (C,n)) /. i) `1 by A10, A11, TOPREAL1:3; then A35: (S-min C) `1 <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 by A3, A8, A9, A17, A18, A19, A20, A21, A32, A30, JORDAN10:3, TOPREAL1:def_12; ((Cage (C,n)) /. (i + 1)) `1 <= p `1 by A10, A11, A34, TOPREAL1:3; then A36: ((Gauge (C,n)) * (i2,1)) `1 <= (S-min C) `1 by A3, A20, A32, A30, TOPREAL1:def_12; A37: 1 <= i2 by A19, MATRIX_1:38; 1 + 1 <= len (Gauge (C,n)) by A6, XXREAL_0:2; then ((Gauge (C,n)) * (1,j1)) `2 <= (S-min C) `2 by A5, A30, A7, A12, SPRECT_3:12; then S-min C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i2,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A30, A12, A36, A35, A4; then S-min C in cell ((Gauge (C,n)),i2,j1) by A5, A30, A37, A33, A7, GOBRD11:32; hence S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A8, A9, A16, A17, A18, A19, A20, A21, A32, A28, GOBRD13:26, JORDAN10:3; ::_thesis: verum end; theorem :: JORDAN1D:14 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i) ) A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; consider i being Element of NAT such that A2: 1 <= i and A3: i < len (Cage (C,n)) and A4: S-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th13; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & S-min C in right_cell ((Cage (C,n)),i) ) thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: S-min C in right_cell ((Cage (C,n)),i) i + 1 <= len (Cage (C,n)) by A3, NAT_1:13; then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33; hence S-min C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum end; theorem Th15: :: JORDAN1D:15 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) consider p being Point of (TOP-REAL 2) such that A1: (south_halfline (S-max C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:88, PSCOMP_1:58; A2: p in (south_halfline (S-max C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1; then A3: p in south_halfline (S-max C) by XBOOLE_0:def_4; A4: S-max C = |[((S-max C) `1),((S-max C) `2)]| by EUCLID:53; A5: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A6: len (Gauge (C,n)) >= 4 by JORDAN8:10; then A7: 1 < len (Gauge (C,n)) by XXREAL_0:2; p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4; then consider i being Element of NAT such that A8: 1 <= i and A9: i + 1 <= len (Cage (C,n)) and A10: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) A11: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A8, A9, TOPREAL1:def_3; A12: (S-max C) `2 = S-bound C by EUCLID:52 .= ((Gauge (C,n)) * (1,2)) `2 by A7, JORDAN8:13 ; A13: S-max C in S-most C by PSCOMP_1:58; thus A14: ( 1 <= i & i < len (Cage (C,n)) ) by A8, A9, NAT_1:13; ::_thesis: S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) then A15: ((Cage (C,n)) /. i) `2 = p `2 by A3, A10, A13, A11, JORDAN1A:80, SPPOL_1:40; A16: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i1, j1, i2, j2 being Element of NAT such that A17: [i1,j1] in Indices (Gauge (C,n)) and A18: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and A19: [i2,j2] in Indices (Gauge (C,n)) and A20: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and A21: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A8, A9, JORDAN8:3; A22: 1 <= i1 by A17, MATRIX_1:38; A23: 1 <= j2 by A19, MATRIX_1:38; A24: i2 <= i2 + 1 by NAT_1:11; A25: j2 <= width (Gauge (C,n)) by A19, MATRIX_1:38; A26: i1 <= len (Gauge (C,n)) by A17, MATRIX_1:38; A27: j1 <= width (Gauge (C,n)) by A17, MATRIX_1:38; p `2 = S-bound (L~ (Cage (C,n))) by A2, JORDAN1A:84, PSCOMP_1:58; then ((Gauge (C,n)) * (i1,j1)) `2 = ((Gauge (C,n)) * (i1,1)) `2 by A18, A15, A22, A26, JORDAN1A:72; then A28: 1 >= j1 by A22, A26, A27, GOBOARD5:4; A29: 1 <= j1 by A17, MATRIX_1:38; then A30: j1 = 1 by A28, XXREAL_0:1; A31: ((Cage (C,n)) /. (i + 1)) `2 = p `2 by A3, A10, A14, A13, A11, JORDAN1A:80, SPPOL_1:40; A32: j1 = j2 proof assume j1 <> j2 ; ::_thesis: contradiction then ( j1 < j2 or j2 < j1 ) by XXREAL_0:1; hence contradiction by A18, A20, A21, A15, A31, A22, A26, A29, A25, A23, A27, GOBOARD5:4; ::_thesis: verum end; then A33: i2 < len (Gauge (C,n)) by A8, A9, A17, A18, A19, A20, A21, A26, A28, JORDAN10:3, NAT_1:13; 1 <= i2 by A19, MATRIX_1:38; then A34: ((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1 by A8, A9, A17, A18, A19, A20, A21, A26, A29, A25, A23, A27, A28, A24, JORDAN10:3, JORDAN1A:18; then p `1 <= ((Cage (C,n)) /. i) `1 by A10, A11, TOPREAL1:3; then A35: (S-max C) `1 <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 by A3, A8, A9, A17, A18, A19, A20, A21, A32, A30, JORDAN10:3, TOPREAL1:def_12; ((Cage (C,n)) /. (i + 1)) `1 <= p `1 by A10, A11, A34, TOPREAL1:3; then A36: ((Gauge (C,n)) * (i2,1)) `1 <= (S-max C) `1 by A3, A20, A32, A30, TOPREAL1:def_12; A37: 1 <= i2 by A19, MATRIX_1:38; 1 + 1 <= len (Gauge (C,n)) by A6, XXREAL_0:2; then ((Gauge (C,n)) * (1,j1)) `2 <= (S-max C) `2 by A5, A30, A7, A12, SPRECT_3:12; then S-max C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i2,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A30, A12, A36, A35, A4; then S-max C in cell ((Gauge (C,n)),i2,j1) by A5, A30, A37, A33, A7, GOBRD11:32; hence S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A8, A9, A16, A17, A18, A19, A20, A21, A32, A28, GOBRD13:26, JORDAN10:3; ::_thesis: verum end; theorem :: JORDAN1D:16 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i) ) A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; consider i being Element of NAT such that A2: 1 <= i and A3: i < len (Cage (C,n)) and A4: S-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th15; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & S-max C in right_cell ((Cage (C,n)),i) ) thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: S-max C in right_cell ((Cage (C,n)),i) i + 1 <= len (Cage (C,n)) by A3, NAT_1:13; then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33; hence S-max C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum end; theorem Th17: :: JORDAN1D:17 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) consider p being Point of (TOP-REAL 2) such that A1: (west_halfline (W-min C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:89, PSCOMP_1:34; A2: p in (west_halfline (W-min C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1; then A3: p in west_halfline (W-min C) by XBOOLE_0:def_4; A4: W-min C = |[((W-min C) `1),((W-min C) `2)]| by EUCLID:53; A5: len (Gauge (C,n)) >= 4 by JORDAN8:10; then A6: 1 < len (Gauge (C,n)) by XXREAL_0:2; A7: (W-min C) `1 = W-bound C by EUCLID:52 .= ((Gauge (C,n)) * (2,1)) `1 by A6, JORDAN8:11 ; A8: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A9: W-min C in W-most C by PSCOMP_1:34; p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4; then consider i being Element of NAT such that A10: 1 <= i and A11: i + 1 <= len (Cage (C,n)) and A12: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) A13: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A10, A11, TOPREAL1:def_3; thus A14: ( 1 <= i & i < len (Cage (C,n)) ) by A10, A11, NAT_1:13; ::_thesis: W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) then A15: ((Cage (C,n)) /. i) `1 = p `1 by A3, A12, A9, A13, JORDAN1A:81, SPPOL_1:41; A16: ((Cage (C,n)) /. (i + 1)) `1 = p `1 by A3, A12, A14, A9, A13, JORDAN1A:81, SPPOL_1:41; A17: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i1, j1, i2, j2 being Element of NAT such that A18: [i1,j1] in Indices (Gauge (C,n)) and A19: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and A20: [i2,j2] in Indices (Gauge (C,n)) and A21: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and A22: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10, A11, JORDAN8:3; A23: i1 <= len (Gauge (C,n)) by A18, MATRIX_1:38; A24: i2 <= len (Gauge (C,n)) by A20, MATRIX_1:38; A25: j2 <= width (Gauge (C,n)) by A20, MATRIX_1:38; A26: j1 <= width (Gauge (C,n)) by A18, MATRIX_1:38; A27: 1 <= j1 by A18, MATRIX_1:38; p `1 = W-bound (L~ (Cage (C,n))) by A2, JORDAN1A:85, PSCOMP_1:34; then ((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (1,j1)) `1 by A19, A15, A8, A27, A26, JORDAN1A:73; then A28: 1 >= i1 by A23, A27, A26, GOBOARD5:3; A29: 1 <= i1 by A18, MATRIX_1:38; then A30: i1 = 1 by A28, XXREAL_0:1; A31: 1 <= i2 by A20, MATRIX_1:38; A32: i1 = i2 proof assume i1 <> i2 ; ::_thesis: contradiction then ( i1 < i2 or i2 < i1 ) by XXREAL_0:1; hence contradiction by A19, A21, A22, A15, A16, A29, A23, A31, A24, A27, A25, GOBOARD5:3; ::_thesis: verum end; then A33: j1 < width (Gauge (C,n)) by A10, A11, A18, A19, A20, A21, A22, A25, A28, JORDAN10:2, NAT_1:13; j1 <= j1 + 1 by NAT_1:11; then A34: ((Cage (C,n)) /. i) `2 <= ((Cage (C,n)) /. (i + 1)) `2 by A10, A11, A18, A19, A20, A21, A22, A29, A23, A27, A25, A32, A28, JORDAN10:2, JORDAN1A:19; then p `2 <= ((Cage (C,n)) /. (i + 1)) `2 by A12, A13, TOPREAL1:4; then A35: (W-min C) `2 <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 by A3, A10, A11, A18, A19, A20, A21, A22, A32, A30, JORDAN10:2, TOPREAL1:def_13; ((Cage (C,n)) /. i) `2 <= p `2 by A12, A13, A34, TOPREAL1:4; then A36: ((Gauge (C,n)) * (1,j1)) `2 <= (W-min C) `2 by A3, A19, A30, TOPREAL1:def_13; 1 + 1 <= len (Gauge (C,n)) by A5, XXREAL_0:2; then ((Gauge (C,n)) * (i1,1)) `1 <= (W-min C) `1 by A8, A30, A6, A7, SPRECT_3:13; then W-min C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A30, A7, A36, A35, A4; then W-min C in cell ((Gauge (C,n)),i1,j1) by A27, A30, A33, A6, GOBRD11:32; hence W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A10, A11, A17, A18, A19, A20, A21, A22, A32, A28, GOBRD13:22, JORDAN10:2; ::_thesis: verum end; theorem :: JORDAN1D:18 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i) ) A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; consider i being Element of NAT such that A2: 1 <= i and A3: i < len (Cage (C,n)) and A4: W-min C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th17; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & W-min C in right_cell ((Cage (C,n)),i) ) thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: W-min C in right_cell ((Cage (C,n)),i) i + 1 <= len (Cage (C,n)) by A3, NAT_1:13; then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33; hence W-min C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum end; theorem Th19: :: JORDAN1D:19 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) consider p being Point of (TOP-REAL 2) such that A1: (west_halfline (W-max C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:89, PSCOMP_1:34; A2: p in (west_halfline (W-max C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def_1; then A3: p in west_halfline (W-max C) by XBOOLE_0:def_4; A4: W-max C = |[((W-max C) `1),((W-max C) `2)]| by EUCLID:53; A5: len (Gauge (C,n)) >= 4 by JORDAN8:10; then A6: 1 < len (Gauge (C,n)) by XXREAL_0:2; A7: (W-max C) `1 = W-bound C by EUCLID:52 .= ((Gauge (C,n)) * (2,1)) `1 by A6, JORDAN8:11 ; A8: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A9: W-max C in W-most C by PSCOMP_1:34; p in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4; then consider i being Element of NAT such that A10: 1 <= i and A11: i + 1 <= len (Cage (C,n)) and A12: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) ) A13: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A10, A11, TOPREAL1:def_3; thus A14: ( 1 <= i & i < len (Cage (C,n)) ) by A10, A11, NAT_1:13; ::_thesis: W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) then A15: ((Cage (C,n)) /. i) `1 = p `1 by A3, A12, A9, A13, JORDAN1A:81, SPPOL_1:41; A16: ((Cage (C,n)) /. (i + 1)) `1 = p `1 by A3, A12, A14, A9, A13, JORDAN1A:81, SPPOL_1:41; A17: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i1, j1, i2, j2 being Element of NAT such that A18: [i1,j1] in Indices (Gauge (C,n)) and A19: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and A20: [i2,j2] in Indices (Gauge (C,n)) and A21: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and A22: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10, A11, JORDAN8:3; A23: i1 <= len (Gauge (C,n)) by A18, MATRIX_1:38; A24: i2 <= len (Gauge (C,n)) by A20, MATRIX_1:38; A25: j2 <= width (Gauge (C,n)) by A20, MATRIX_1:38; A26: j1 <= width (Gauge (C,n)) by A18, MATRIX_1:38; A27: 1 <= j1 by A18, MATRIX_1:38; p `1 = W-bound (L~ (Cage (C,n))) by A2, JORDAN1A:85, PSCOMP_1:34; then ((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (1,j1)) `1 by A19, A15, A8, A27, A26, JORDAN1A:73; then A28: 1 >= i1 by A23, A27, A26, GOBOARD5:3; A29: 1 <= i1 by A18, MATRIX_1:38; then A30: i1 = 1 by A28, XXREAL_0:1; A31: 1 <= i2 by A20, MATRIX_1:38; A32: i1 = i2 proof assume i1 <> i2 ; ::_thesis: contradiction then ( i1 < i2 or i2 < i1 ) by XXREAL_0:1; hence contradiction by A19, A21, A22, A15, A16, A29, A23, A31, A24, A27, A25, GOBOARD5:3; ::_thesis: verum end; then A33: j1 < width (Gauge (C,n)) by A10, A11, A18, A19, A20, A21, A22, A25, A28, JORDAN10:2, NAT_1:13; j1 <= j1 + 1 by NAT_1:11; then A34: ((Cage (C,n)) /. i) `2 <= ((Cage (C,n)) /. (i + 1)) `2 by A10, A11, A18, A19, A20, A21, A22, A29, A23, A27, A25, A32, A28, JORDAN10:2, JORDAN1A:19; then p `2 <= ((Cage (C,n)) /. (i + 1)) `2 by A12, A13, TOPREAL1:4; then A35: (W-max C) `2 <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 by A3, A10, A11, A18, A19, A20, A21, A22, A32, A30, JORDAN10:2, TOPREAL1:def_13; ((Cage (C,n)) /. i) `2 <= p `2 by A12, A13, A34, TOPREAL1:4; then A36: ((Gauge (C,n)) * (1,j1)) `2 <= (W-max C) `2 by A3, A19, A30, TOPREAL1:def_13; 1 + 1 <= len (Gauge (C,n)) by A5, XXREAL_0:2; then ((Gauge (C,n)) * (i1,1)) `1 <= (W-max C) `1 by A8, A30, A6, A7, SPRECT_3:13; then W-max C in { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A30, A7, A36, A35, A4; then W-max C in cell ((Gauge (C,n)),i1,j1) by A27, A30, A33, A6, GOBRD11:32; hence W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A10, A11, A17, A18, A19, A20, A21, A22, A32, A28, GOBRD13:22, JORDAN10:2; ::_thesis: verum end; theorem :: JORDAN1D:20 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i) ) A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; consider i being Element of NAT such that A2: 1 <= i and A3: i < len (Cage (C,n)) and A4: W-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by Th19; take i ; ::_thesis: ( 1 <= i & i < len (Cage (C,n)) & W-max C in right_cell ((Cage (C,n)),i) ) thus ( 1 <= i & i < len (Cage (C,n)) ) by A2, A3; ::_thesis: W-max C in right_cell ((Cage (C,n)),i) i + 1 <= len (Cage (C,n)) by A3, NAT_1:13; then right_cell ((Cage (C,n)),i,(Gauge (C,n))) c= right_cell ((Cage (C,n)),i) by A2, A1, GOBRD13:33; hence W-max C in right_cell ((Cage (C,n)),i) by A4; ::_thesis: verum end; theorem Th21: :: JORDAN1D:21 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) ) A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; N-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:39; then consider m being Nat such that A2: m in dom (Cage (C,n)) and A3: (Cage (C,n)) . m = N-min (L~ (Cage (C,n))) by FINSEQ_2:10; A4: (Cage (C,n)) /. m = N-min (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def_6; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i, j being Element of NAT such that A5: [i,j] in Indices (Gauge (C,n)) and A6: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A2, GOBOARD1:def_9; take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) ) thus A7: ( 1 <= i & i <= len (Gauge (C,n)) ) by A5, MATRIX_1:38; ::_thesis: N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) A8: 1 <= j by A5, MATRIX_1:38; A9: now__::_thesis:_not_j_<_width_(Gauge_(C,n)) assume j < width (Gauge (C,n)) ; ::_thesis: contradiction then (N-min (L~ (Cage (C,n)))) `2 < ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 by A4, A6, A7, A8, GOBOARD5:4; then N-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 by EUCLID:52; hence contradiction by A7, A1, JORDAN1A:70; ::_thesis: verum end; j <= width (Gauge (C,n)) by A5, MATRIX_1:38; hence N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) by A4, A6, A9, XXREAL_0:1; ::_thesis: verum end; theorem :: JORDAN1D:22 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) ) A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; N-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:40; then consider m being Nat such that A2: m in dom (Cage (C,n)) and A3: (Cage (C,n)) . m = N-max (L~ (Cage (C,n))) by FINSEQ_2:10; A4: (Cage (C,n)) /. m = N-max (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def_6; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i, j being Element of NAT such that A5: [i,j] in Indices (Gauge (C,n)) and A6: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A2, GOBOARD1:def_9; take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) ) thus A7: ( 1 <= i & i <= len (Gauge (C,n)) ) by A5, MATRIX_1:38; ::_thesis: N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) A8: 1 <= j by A5, MATRIX_1:38; A9: now__::_thesis:_not_j_<_width_(Gauge_(C,n)) assume j < width (Gauge (C,n)) ; ::_thesis: contradiction then (N-max (L~ (Cage (C,n)))) `2 < ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 by A4, A6, A7, A8, GOBOARD5:4; then N-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 by EUCLID:52; hence contradiction by A7, A1, JORDAN1A:70; ::_thesis: verum end; j <= width (Gauge (C,n)) by A5, MATRIX_1:38; hence N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) by A4, A6, A9, XXREAL_0:1; ::_thesis: verum end; theorem :: JORDAN1D:23 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Cage (C,n)) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Cage (C,n)) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Cage (C,n)) ) consider i being Element of NAT such that A1: 1 <= i and A2: i <= len (Gauge (C,n)) and A3: N-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) by Th21; take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Cage (C,n)) ) thus ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Cage (C,n)) ) by A1, A2, A3, SPRECT_2:39; ::_thesis: verum end; theorem Th24: :: JORDAN1D:24 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) ) A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; E-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:45; then consider m being Nat such that A2: m in dom (Cage (C,n)) and A3: (Cage (C,n)) . m = E-min (L~ (Cage (C,n))) by FINSEQ_2:10; A4: (Cage (C,n)) /. m = E-min (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def_6; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i, j being Element of NAT such that A5: [i,j] in Indices (Gauge (C,n)) and A6: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A2, GOBOARD1:def_9; take j ; ::_thesis: ( 1 <= j & j <= width (Gauge (C,n)) & E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) ) thus A7: ( 1 <= j & j <= width (Gauge (C,n)) ) by A5, MATRIX_1:38; ::_thesis: E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) A8: 1 <= i by A5, MATRIX_1:38; A9: now__::_thesis:_not_i_<_len_(Gauge_(C,n)) assume i < len (Gauge (C,n)) ; ::_thesis: contradiction then (E-min (L~ (Cage (C,n)))) `1 < ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by A4, A6, A7, A8, GOBOARD5:3; then E-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by EUCLID:52; hence contradiction by A7, A1, JORDAN1A:71; ::_thesis: verum end; i <= len (Gauge (C,n)) by A5, MATRIX_1:38; hence E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by A4, A6, A9, XXREAL_0:1; ::_thesis: verum end; theorem :: JORDAN1D:25 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) ) A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46; then consider m being Nat such that A2: m in dom (Cage (C,n)) and A3: (Cage (C,n)) . m = E-max (L~ (Cage (C,n))) by FINSEQ_2:10; A4: (Cage (C,n)) /. m = E-max (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def_6; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i, j being Element of NAT such that A5: [i,j] in Indices (Gauge (C,n)) and A6: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A2, GOBOARD1:def_9; take j ; ::_thesis: ( 1 <= j & j <= width (Gauge (C,n)) & E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) ) thus A7: ( 1 <= j & j <= width (Gauge (C,n)) ) by A5, MATRIX_1:38; ::_thesis: E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) A8: 1 <= i by A5, MATRIX_1:38; A9: now__::_thesis:_not_i_<_len_(Gauge_(C,n)) assume i < len (Gauge (C,n)) ; ::_thesis: contradiction then (E-max (L~ (Cage (C,n)))) `1 < ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by A4, A6, A7, A8, GOBOARD5:3; then E-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by EUCLID:52; hence contradiction by A7, A1, JORDAN1A:71; ::_thesis: verum end; i <= len (Gauge (C,n)) by A5, MATRIX_1:38; hence E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by A4, A6, A9, XXREAL_0:1; ::_thesis: verum end; theorem :: JORDAN1D:26 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * ((len (Gauge (C,n))),j) in rng (Cage (C,n)) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * ((len (Gauge (C,n))),j) in rng (Cage (C,n)) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * ((len (Gauge (C,n))),j) in rng (Cage (C,n)) ) consider j being Element of NAT such that A1: 1 <= j and A2: j <= width (Gauge (C,n)) and A3: E-min (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by Th24; take j ; ::_thesis: ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * ((len (Gauge (C,n))),j) in rng (Cage (C,n)) ) thus ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * ((len (Gauge (C,n))),j) in rng (Cage (C,n)) ) by A1, A2, A3, SPRECT_2:45; ::_thesis: verum end; theorem Th27: :: JORDAN1D:27 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) ) S-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:41; then consider m being Nat such that A1: m in dom (Cage (C,n)) and A2: (Cage (C,n)) . m = S-min (L~ (Cage (C,n))) by FINSEQ_2:10; A3: (Cage (C,n)) /. m = S-min (L~ (Cage (C,n))) by A1, A2, PARTFUN1:def_6; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i, j being Element of NAT such that A4: [i,j] in Indices (Gauge (C,n)) and A5: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A1, GOBOARD1:def_9; take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) ) thus A6: ( 1 <= i & i <= len (Gauge (C,n)) ) by A4, MATRIX_1:38; ::_thesis: S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) A7: j <= width (Gauge (C,n)) by A4, MATRIX_1:38; A8: now__::_thesis:_not_j_>_1 assume j > 1 ; ::_thesis: contradiction then (S-min (L~ (Cage (C,n)))) `2 > ((Gauge (C,n)) * (i,1)) `2 by A3, A5, A6, A7, GOBOARD5:4; then S-bound (L~ (Cage (C,n))) > ((Gauge (C,n)) * (i,1)) `2 by EUCLID:52; hence contradiction by A6, JORDAN1A:72; ::_thesis: verum end; 1 <= j by A4, MATRIX_1:38; hence S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) by A3, A5, A8, XXREAL_0:1; ::_thesis: verum end; theorem :: JORDAN1D:28 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) ) S-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:42; then consider m being Nat such that A1: m in dom (Cage (C,n)) and A2: (Cage (C,n)) . m = S-max (L~ (Cage (C,n))) by FINSEQ_2:10; A3: (Cage (C,n)) /. m = S-max (L~ (Cage (C,n))) by A1, A2, PARTFUN1:def_6; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i, j being Element of NAT such that A4: [i,j] in Indices (Gauge (C,n)) and A5: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A1, GOBOARD1:def_9; take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) ) thus A6: ( 1 <= i & i <= len (Gauge (C,n)) ) by A4, MATRIX_1:38; ::_thesis: S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) A7: j <= width (Gauge (C,n)) by A4, MATRIX_1:38; A8: now__::_thesis:_not_j_>_1 assume j > 1 ; ::_thesis: contradiction then (S-max (L~ (Cage (C,n)))) `2 > ((Gauge (C,n)) * (i,1)) `2 by A3, A5, A6, A7, GOBOARD5:4; then S-bound (L~ (Cage (C,n))) > ((Gauge (C,n)) * (i,1)) `2 by EUCLID:52; hence contradiction by A6, JORDAN1A:72; ::_thesis: verum end; 1 <= j by A4, MATRIX_1:38; hence S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) by A3, A5, A8, XXREAL_0:1; ::_thesis: verum end; theorem :: JORDAN1D:29 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,1) in rng (Cage (C,n)) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,1) in rng (Cage (C,n)) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,1) in rng (Cage (C,n)) ) consider i being Element of NAT such that A1: 1 <= i and A2: i <= len (Gauge (C,n)) and A3: S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) by Th27; take i ; ::_thesis: ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,1) in rng (Cage (C,n)) ) thus ( 1 <= i & i <= len (Gauge (C,n)) & (Gauge (C,n)) * (i,1) in rng (Cage (C,n)) ) by A1, A2, A3, SPRECT_2:41; ::_thesis: verum end; theorem Th30: :: JORDAN1D:30 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) ) A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43; then consider m being Nat such that A2: m in dom (Cage (C,n)) and A3: (Cage (C,n)) . m = W-min (L~ (Cage (C,n))) by FINSEQ_2:10; A4: (Cage (C,n)) /. m = W-min (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def_6; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i, j being Element of NAT such that A5: [i,j] in Indices (Gauge (C,n)) and A6: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A2, GOBOARD1:def_9; take j ; ::_thesis: ( 1 <= j & j <= width (Gauge (C,n)) & W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) ) thus A7: ( 1 <= j & j <= width (Gauge (C,n)) ) by A5, MATRIX_1:38; ::_thesis: W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) A8: i <= len (Gauge (C,n)) by A5, MATRIX_1:38; A9: now__::_thesis:_not_i_>_1 assume i > 1 ; ::_thesis: contradiction then (W-min (L~ (Cage (C,n)))) `1 > ((Gauge (C,n)) * (1,j)) `1 by A4, A6, A7, A8, GOBOARD5:3; then W-bound (L~ (Cage (C,n))) > ((Gauge (C,n)) * (1,j)) `1 by EUCLID:52; hence contradiction by A7, A1, JORDAN1A:73; ::_thesis: verum end; 1 <= i by A5, MATRIX_1:38; hence W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) by A4, A6, A9, XXREAL_0:1; ::_thesis: verum end; theorem :: JORDAN1D:31 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) ) A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; W-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:44; then consider m being Nat such that A2: m in dom (Cage (C,n)) and A3: (Cage (C,n)) . m = W-max (L~ (Cage (C,n))) by FINSEQ_2:10; A4: (Cage (C,n)) /. m = W-max (L~ (Cage (C,n))) by A2, A3, PARTFUN1:def_6; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i, j being Element of NAT such that A5: [i,j] in Indices (Gauge (C,n)) and A6: (Cage (C,n)) /. m = (Gauge (C,n)) * (i,j) by A2, GOBOARD1:def_9; take j ; ::_thesis: ( 1 <= j & j <= width (Gauge (C,n)) & W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) ) thus A7: ( 1 <= j & j <= width (Gauge (C,n)) ) by A5, MATRIX_1:38; ::_thesis: W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) A8: i <= len (Gauge (C,n)) by A5, MATRIX_1:38; A9: now__::_thesis:_not_i_>_1 assume i > 1 ; ::_thesis: contradiction then (W-max (L~ (Cage (C,n)))) `1 > ((Gauge (C,n)) * (1,j)) `1 by A4, A6, A7, A8, GOBOARD5:3; then W-bound (L~ (Cage (C,n))) > ((Gauge (C,n)) * (1,j)) `1 by EUCLID:52; hence contradiction by A7, A1, JORDAN1A:73; ::_thesis: verum end; 1 <= i by A5, MATRIX_1:38; hence W-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) by A4, A6, A9, XXREAL_0:1; ::_thesis: verum end; theorem :: JORDAN1D:32 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (1,j) in rng (Cage (C,n)) ) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (1,j) in rng (Cage (C,n)) ) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ex j being Element of NAT st ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (1,j) in rng (Cage (C,n)) ) consider j being Element of NAT such that A1: 1 <= j and A2: j <= width (Gauge (C,n)) and A3: W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) by Th30; take j ; ::_thesis: ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (1,j) in rng (Cage (C,n)) ) thus ( 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (1,j) in rng (Cage (C,n)) ) by A1, A2, A3, SPRECT_2:43; ::_thesis: verum end;