jordan5d.miz



    begin

    reserve p,q for Point of ( TOP-REAL 2),

r for Real,

h for non constant standard special_circular_sequence,

g for FinSequence of ( TOP-REAL 2),

f for non empty FinSequence of ( TOP-REAL 2),

I,i1,i,j,k for Nat;

    theorem :: JORDAN5D:1

    

     Th1: for n be Nat, h be FinSequence of ( TOP-REAL n) st ( len h) >= 2 holds (h /. ( len h)) in ( LSeg (h,(( len h) -' 1)))

    proof

      let n be Nat;

      let h be FinSequence of ( TOP-REAL n);

      set i = ( len h);

      assume

       A1: ( len h) >= 2;

      then

       A2: (2 - 1) <= (i - 1) by XREAL_1: 9;

      ((i -' 1) + 1) = ( len h) by A1, XREAL_1: 235, XXREAL_0: 2;

      hence thesis by A2, TOPREAL1: 21;

    end;

    theorem :: JORDAN5D:2

    

     Th2: 3 <= i implies (i mod (i -' 1)) = 1

    proof

      assume

       A1: 3 <= i;

      then

       A2: (i -' 1) = (i - 1) by XREAL_1: 233, XXREAL_0: 2;

      (3 -' 1) = ((2 + 1) -' 1)

      .= 2 by NAT_D: 34;

      then 2 <= (i -' 1) by A1, NAT_D: 42;

      then 1 < (i - 1) by A2, XXREAL_0: 2;

      then (1 + i) < ((i - 1) + i) by XREAL_1: 8;

      then ((1 + i) - 1) < (((i - 1) + i) - 1) by XREAL_1: 14;

      then

       A3: i < ((i - 1) + (i - 1));

      (i -' 1) <= i by NAT_D: 35;

      

      hence (i mod (i -' 1)) = (i - (i - 1)) by A2, A3, JORDAN4: 2

      .= 1;

    end;

    theorem :: JORDAN5D:3

    

     Th3: p in ( rng h) implies ex i be Nat st 1 <= i & (i + 1) <= ( len h) & (h . i) = p

    proof

      

       A1: 4 < ( len h) by GOBOARD7: 34;

      

       A2: 1 < ( len h) by GOBOARD7: 34, XXREAL_0: 2;

      assume p in ( rng h);

      then

      consider x be object such that

       A3: x in ( dom h) and

       A4: p = (h . x) by FUNCT_1:def 3;

      reconsider i = x as Nat by A3;

      

       A5: 1 <= i by A3, FINSEQ_3: 25;

      set j = ( S_Drop (i,h));

      

       A6: i <= ( len h) by A3, FINSEQ_3: 25;

      1 <= j & (j + 1) <= ( len h) & (h . j) = p

      proof

        

         A7: i <= ((( len h) -' 1) + 1) by A5, A6, XREAL_1: 235, XXREAL_0: 2;

        per cases by A7, NAT_1: 8;

          suppose

           A8: i <= (( len h) -' 1);

          then j = i by A5, JORDAN4: 22;

          then (j + 1) <= ((( len h) -' 1) + 1) by A8, XREAL_1: 7;

          hence thesis by A4, A5, A2, A8, JORDAN4: 22, XREAL_1: 235;

        end;

          suppose

           A9: i = ((( len h) -' 1) + 1);

          then i = ( len h) by A1, XREAL_1: 235, XXREAL_0: 2;

          then (i mod (( len h) -' 1)) = 1 by A1, Th2, XXREAL_0: 2;

          then

           A10: j = 1 by JORDAN4:def 1;

          

           A11: 1 <= ( len h) by GOBOARD7: 34, XXREAL_0: 2;

          then

           A12: ( len h) in ( dom h) by FINSEQ_3: 25;

          1 in ( dom h) by A11, FINSEQ_3: 25;

          

          then (h . 1) = (h /. 1) by PARTFUN1:def 6

          .= (h /. ( len h)) by FINSEQ_6:def 1

          .= (h . ( len h)) by A12, PARTFUN1:def 6;

          hence thesis by A4, A1, A9, A10, XREAL_1: 235, XXREAL_0: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN5D:4

    

     Th4: for g be FinSequence of REAL st r in ( rng g) holds (( Incr g) . 1) <= r & r <= (( Incr g) . ( len ( Incr g)))

    proof

      let g be FinSequence of REAL ;

      assume r in ( rng g);

      then r in ( rng ( Incr g)) by SEQ_4:def 21;

      then

      consider x be object such that

       A1: x in ( dom ( Incr g)) and

       A2: (( Incr g) . x) = r by FUNCT_1:def 3;

      reconsider j = x as Nat by A1;

      

       A3: x in ( Seg ( len ( Incr g))) by A1, FINSEQ_1:def 3;

      then

       A4: j <= ( len ( Incr g)) by FINSEQ_1: 1;

      

       A5: 1 <= j by A3, FINSEQ_1: 1;

      then

       A6: 1 <= ( len ( Incr g)) by A4, XXREAL_0: 2;

      then 1 in ( dom ( Incr g)) by FINSEQ_3: 25;

      hence (( Incr g) . 1) <= r by A1, A2, A5, SEQ_4: 137;

      ( len ( Incr g)) in ( dom ( Incr g)) by A6, FINSEQ_3: 25;

      hence thesis by A1, A2, A4, SEQ_4: 137;

    end;

    theorem :: JORDAN5D:5

    

     Th5: 1 <= i & i <= ( len h) & 1 <= I & I <= ( width ( GoB h)) implies ((( GoB h) * (1,I)) `1 ) <= ((h /. i) `1 ) & ((h /. i) `1 ) <= ((( GoB h) * (( len ( GoB h)),I)) `1 )

    proof

      assume that

       A1: 1 <= i and

       A2: i <= ( len h) and

       A3: 1 <= I and

       A4: I <= ( width ( GoB h));

      

       A5: I <= ( width ( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h))))) by A4, GOBOARD2:def 2;

      i <= ( len ( X_axis h)) by A2, GOBOARD1:def 1;

      then

       A6: i in ( dom ( X_axis h)) by A1, FINSEQ_3: 25;

      then (( X_axis h) . i) = ((h /. i) `1 ) by GOBOARD1:def 1;

      then

       A7: ((h /. i) `1 ) in ( rng ( X_axis h)) by A6, FUNCT_1:def 3;

      

       A8: ( GoB h) = ( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h)))) by GOBOARD2:def 2;

      then 1 <= ( len ( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h))))) by GOBOARD7: 32;

      then

       A9: [1, I] in ( Indices ( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h))))) by A3, A5, MATRIX_0: 30;

      

       A10: 1 <= ( len ( GoB h)) by GOBOARD7: 32;

      ( len ( GoB h)) <= ( len ( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h))))) by GOBOARD2:def 2;

      then

       A11: [( len ( GoB h)), I] in ( Indices ( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h))))) by A3, A5, A10, MATRIX_0: 30;

      (( GoB h) * (( len ( GoB h)),I)) = (( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h)))) * (( len ( GoB h)),I)) by GOBOARD2:def 2

      .= |[(( Incr ( X_axis h)) . ( len ( GoB h))), (( Incr ( Y_axis h)) . I)]| by A11, GOBOARD2:def 1;

      then

       A12: ((( GoB h) * (( len ( GoB h)),I)) `1 ) = (( Incr ( X_axis h)) . ( len ( GoB h))) by EUCLID: 52;

      (( GoB h) * (1,I)) = (( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h)))) * (1,I)) by GOBOARD2:def 2

      .= |[(( Incr ( X_axis h)) . 1), (( Incr ( Y_axis h)) . I)]| by A9, GOBOARD2:def 1;

      then

       A13: ((( GoB h) * (1,I)) `1 ) = (( Incr ( X_axis h)) . 1) by EUCLID: 52;

      ( len ( GoB h)) = ( len ( Incr ( X_axis h))) by A8, GOBOARD2:def 1;

      hence thesis by A12, A13, A7, Th4;

    end;

    theorem :: JORDAN5D:6

    

     Th6: 1 <= i & i <= ( len h) & 1 <= I & I <= ( len ( GoB h)) implies ((( GoB h) * (I,1)) `2 ) <= ((h /. i) `2 ) & ((h /. i) `2 ) <= ((( GoB h) * (I,( width ( GoB h)))) `2 )

    proof

      assume that

       A1: 1 <= i and

       A2: i <= ( len h) and

       A3: 1 <= I and

       A4: I <= ( len ( GoB h));

      

       A5: ( GoB h) = ( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h)))) by GOBOARD2:def 2;

      then

       A6: 1 <= ( width ( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h))))) by GOBOARD7: 33;

      i <= ( len ( Y_axis h)) by A2, GOBOARD1:def 2;

      then

       A7: i in ( dom ( Y_axis h)) by A1, FINSEQ_3: 25;

      then (( Y_axis h) . i) = ((h /. i) `2 ) by GOBOARD1:def 2;

      then

       A8: ((h /. i) `2 ) in ( rng ( Y_axis h)) by A7, FUNCT_1:def 3;

      1 <= ( width ( GoB h)) by GOBOARD7: 33;

      then

       A9: [I, ( width ( GoB h))] in ( Indices ( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h))))) by A3, A4, A5, MATRIX_0: 30;

      (( GoB h) * (I,( width ( GoB h)))) = (( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h)))) * (I,( width ( GoB h)))) by GOBOARD2:def 2

      .= |[(( Incr ( X_axis h)) . I), (( Incr ( Y_axis h)) . ( width ( GoB h)))]| by A9, GOBOARD2:def 1;

      then

       A10: ((( GoB h) * (I,( width ( GoB h)))) `2 ) = (( Incr ( Y_axis h)) . ( width ( GoB h))) by EUCLID: 52;

      I <= ( len ( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h))))) by A4, GOBOARD2:def 2;

      then

       A11: [I, 1] in ( Indices ( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h))))) by A3, A6, MATRIX_0: 30;

      (( GoB h) * (I,1)) = (( GoB (( Incr ( X_axis h)),( Incr ( Y_axis h)))) * (I,1)) by GOBOARD2:def 2

      .= |[(( Incr ( X_axis h)) . I), (( Incr ( Y_axis h)) . 1)]| by A11, GOBOARD2:def 1;

      then

       A12: ((( GoB h) * (I,1)) `2 ) = (( Incr ( Y_axis h)) . 1) by EUCLID: 52;

      ( width ( GoB h)) = ( len ( Incr ( Y_axis h))) by A5, GOBOARD2:def 1;

      hence thesis by A10, A12, A8, Th4;

    end;

    theorem :: JORDAN5D:7

    

     Th7: 1 <= i & i <= ( len ( GoB f)) implies ex k, j st k in ( dom f) & [i, j] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * (i,j))

    proof

      assume that

       A1: 1 <= i and

       A2: i <= ( len ( GoB f));

      

       A3: i in ( dom ( GoB f)) by A1, A2, FINSEQ_3: 25;

      

       A4: ( GoB f) = ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) by GOBOARD2:def 2;

      then ( len ( Incr ( X_axis f))) = ( len ( GoB f)) by GOBOARD2:def 1;

      then i in ( dom ( Incr ( X_axis f))) by A1, A2, FINSEQ_3: 25;

      then (( Incr ( X_axis f)) . i) in ( rng ( Incr ( X_axis f))) by FUNCT_1:def 3;

      then (( Incr ( X_axis f)) . i) in ( rng ( X_axis f)) by SEQ_4:def 21;

      then

      consider k be Nat such that

       A5: k in ( dom ( X_axis f)) and

       A6: (( X_axis f) . k) = (( Incr ( X_axis f)) . i) by FINSEQ_2: 10;

      

       A7: ( len ( X_axis f)) = ( len f) by GOBOARD1:def 1

      .= ( len ( Y_axis f)) by GOBOARD1:def 2;

      then ( dom ( X_axis f)) = ( dom ( Y_axis f)) by FINSEQ_3: 29;

      then (( Y_axis f) . k) in ( rng ( Y_axis f)) by A5, FUNCT_1:def 3;

      then (( Y_axis f) . k) in ( rng ( Incr ( Y_axis f))) by SEQ_4:def 21;

      then

      consider j be Nat such that

       A8: j in ( dom ( Incr ( Y_axis f))) and

       A9: (( Y_axis f) . k) = (( Incr ( Y_axis f)) . j) by FINSEQ_2: 10;

      reconsider k, j as Nat;

      

       A10: (( X_axis f) . k) = ((f /. k) `1 ) by A5, GOBOARD1:def 1;

      take k, j;

      ( len ( X_axis f)) = ( len f) by GOBOARD1:def 1;

      hence k in ( dom f) by A5, FINSEQ_3: 29;

      j in ( Seg ( len ( Incr ( Y_axis f)))) by A8, FINSEQ_1:def 3;

      then j in ( Seg ( width ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))))) by GOBOARD2:def 1;

      then [i, j] in [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] by A4, A3, ZFMISC_1: 87;

      hence

       A11: [i, j] in ( Indices ( GoB f)) by MATRIX_0:def 4;

      ( dom ( X_axis f)) = ( dom ( Y_axis f)) by A7, FINSEQ_3: 29;

      then (( Y_axis f) . k) = ((f /. k) `2 ) by A5, GOBOARD1:def 2;

      

      hence (f /. k) = |[(( Incr ( X_axis f)) . i), (( Incr ( Y_axis f)) . j)]| by A6, A9, A10, EUCLID: 53

      .= (( GoB f) * (i,j)) by A4, A11, GOBOARD2:def 1;

    end;

    theorem :: JORDAN5D:8

    

     Th8: 1 <= j & j <= ( width ( GoB f)) implies ex k, i st k in ( dom f) & [i, j] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * (i,j))

    proof

      assume that

       A1: 1 <= j and

       A2: j <= ( width ( GoB f));

      

       A3: j in ( Seg ( width ( GoB f))) by A1, A2, FINSEQ_1: 1;

      

       A4: ( GoB f) = ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) by GOBOARD2:def 2;

      then ( len ( Incr ( Y_axis f))) = ( width ( GoB f)) by GOBOARD2:def 1;

      then j in ( dom ( Incr ( Y_axis f))) by A1, A2, FINSEQ_3: 25;

      then (( Incr ( Y_axis f)) . j) in ( rng ( Incr ( Y_axis f))) by FUNCT_1:def 3;

      then (( Incr ( Y_axis f)) . j) in ( rng ( Y_axis f)) by SEQ_4:def 21;

      then

      consider k be Nat such that

       A5: k in ( dom ( Y_axis f)) and

       A6: (( Y_axis f) . k) = (( Incr ( Y_axis f)) . j) by FINSEQ_2: 10;

      

       A7: ( len ( X_axis f)) = ( len f) by GOBOARD1:def 1

      .= ( len ( Y_axis f)) by GOBOARD1:def 2;

      then k in ( dom ( X_axis f)) by A5, FINSEQ_3: 29;

      then (( X_axis f) . k) in ( rng ( X_axis f)) by FUNCT_1:def 3;

      then (( X_axis f) . k) in ( rng ( Incr ( X_axis f))) by SEQ_4:def 21;

      then

      consider i be Nat such that

       A8: i in ( dom ( Incr ( X_axis f))) and

       A9: (( X_axis f) . k) = (( Incr ( X_axis f)) . i) by FINSEQ_2: 10;

      reconsider k, i as Nat;

      k in ( dom ( X_axis f)) by A5, A7, FINSEQ_3: 29;

      then

       A10: (( X_axis f) . k) = ((f /. k) `1 ) by GOBOARD1:def 1;

      take k, i;

      ( len ( Y_axis f)) = ( len f) by GOBOARD1:def 2;

      hence k in ( dom f) by A5, FINSEQ_3: 29;

      ( len ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f))))) = ( len ( Incr ( X_axis f))) by GOBOARD2:def 1;

      then i in ( dom ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f))))) by A8, FINSEQ_3: 29;

      then [i, j] in [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] by A4, A3, ZFMISC_1: 87;

      hence

       A11: [i, j] in ( Indices ( GoB f)) by MATRIX_0:def 4;

      (( Y_axis f) . k) = ((f /. k) `2 ) by A5, GOBOARD1:def 2;

      

      hence (f /. k) = |[(( Incr ( X_axis f)) . i), (( Incr ( Y_axis f)) . j)]| by A6, A9, A10, EUCLID: 53

      .= (( GoB f) * (i,j)) by A4, A11, GOBOARD2:def 1;

    end;

    theorem :: JORDAN5D:9

    

     Th9: 1 <= i & i <= ( len ( GoB f)) & 1 <= j & j <= ( width ( GoB f)) implies ex k st k in ( dom f) & [i, j] in ( Indices ( GoB f)) & ((f /. k) `1 ) = ((( GoB f) * (i,j)) `1 )

    proof

      assume that

       A1: 1 <= i and

       A2: i <= ( len ( GoB f)) and

       A3: 1 <= j and

       A4: j <= ( width ( GoB f));

      

       A5: ( GoB f) = ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) by GOBOARD2:def 2;

      then ( len ( Incr ( Y_axis f))) = ( width ( GoB f)) by GOBOARD2:def 1;

      then j in ( dom ( Incr ( Y_axis f))) by A3, A4, FINSEQ_3: 25;

      then j in ( Seg ( len ( Incr ( Y_axis f)))) by FINSEQ_1:def 3;

      then

       A6: j in ( Seg ( width ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))))) by GOBOARD2:def 1;

      ( len ( Incr ( X_axis f))) = ( len ( GoB f)) by A5, GOBOARD2:def 1;

      then i in ( dom ( Incr ( X_axis f))) by A1, A2, FINSEQ_3: 25;

      then (( Incr ( X_axis f)) . i) in ( rng ( Incr ( X_axis f))) by FUNCT_1:def 3;

      then (( Incr ( X_axis f)) . i) in ( rng ( X_axis f)) by SEQ_4:def 21;

      then

      consider k be Nat such that

       A7: k in ( dom ( X_axis f)) and

       A8: (( X_axis f) . k) = (( Incr ( X_axis f)) . i) by FINSEQ_2: 10;

      reconsider k as Nat;

      take k;

      ( len ( X_axis f)) = ( len f) by GOBOARD1:def 1;

      hence k in ( dom f) by A7, FINSEQ_3: 29;

      i in ( dom ( GoB f)) by A1, A2, FINSEQ_3: 25;

      then [i, j] in [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] by A5, A6, ZFMISC_1: 87;

      hence [i, j] in ( Indices ( GoB f)) by MATRIX_0:def 4;

      then

       A9: (( GoB f) * (i,j)) = |[(( Incr ( X_axis f)) . i), (( Incr ( Y_axis f)) . j)]| by A5, GOBOARD2:def 1;

      

      thus ((f /. k) `1 ) = (( Incr ( X_axis f)) . i) by A7, A8, GOBOARD1:def 1

      .= ((( GoB f) * (i,j)) `1 ) by A9, EUCLID: 52;

    end;

    theorem :: JORDAN5D:10

    

     Th10: 1 <= i & i <= ( len ( GoB f)) & 1 <= j & j <= ( width ( GoB f)) implies ex k st k in ( dom f) & [i, j] in ( Indices ( GoB f)) & ((f /. k) `2 ) = ((( GoB f) * (i,j)) `2 )

    proof

      assume that

       A1: 1 <= i and

       A2: i <= ( len ( GoB f)) and

       A3: 1 <= j and

       A4: j <= ( width ( GoB f));

      

       A5: ( GoB f) = ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) by GOBOARD2:def 2;

      then ( len ( Incr ( Y_axis f))) = ( width ( GoB f)) by GOBOARD2:def 1;

      then j in ( dom ( Incr ( Y_axis f))) by A3, A4, FINSEQ_3: 25;

      then j in ( Seg ( len ( Incr ( Y_axis f)))) by FINSEQ_1:def 3;

      then

       A6: j in ( Seg ( width ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))))) by GOBOARD2:def 1;

      ( len ( Incr ( Y_axis f))) = ( width ( GoB f)) by A5, GOBOARD2:def 1;

      then j in ( dom ( Incr ( Y_axis f))) by A3, A4, FINSEQ_3: 25;

      then (( Incr ( Y_axis f)) . j) in ( rng ( Incr ( Y_axis f))) by FUNCT_1:def 3;

      then (( Incr ( Y_axis f)) . j) in ( rng ( Y_axis f)) by SEQ_4:def 21;

      then

      consider k be Nat such that

       A7: k in ( dom ( Y_axis f)) and

       A8: (( Y_axis f) . k) = (( Incr ( Y_axis f)) . j) by FINSEQ_2: 10;

      reconsider k as Nat;

      take k;

      ( len ( Y_axis f)) = ( len f) by GOBOARD1:def 2;

      hence k in ( dom f) by A7, FINSEQ_3: 29;

      i in ( dom ( GoB f)) by A1, A2, FINSEQ_3: 25;

      then [i, j] in [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] by A5, A6, ZFMISC_1: 87;

      hence [i, j] in ( Indices ( GoB f)) by MATRIX_0:def 4;

      then

       A9: (( GoB f) * (i,j)) = |[(( Incr ( X_axis f)) . i), (( Incr ( Y_axis f)) . j)]| by A5, GOBOARD2:def 1;

      

      thus ((f /. k) `2 ) = (( Incr ( Y_axis f)) . j) by A7, A8, GOBOARD1:def 2

      .= ((( GoB f) * (i,j)) `2 ) by A9, EUCLID: 52;

    end;

    begin

    theorem :: JORDAN5D:11

    

     Th11: 1 <= i & i <= ( len h) implies ( S-bound ( L~ h)) <= ((h /. i) `2 ) & ((h /. i) `2 ) <= ( N-bound ( L~ h))

    proof

      

       A1: ( len h) > 4 by GOBOARD7: 34;

      assume that

       A2: 1 <= i and

       A3: i <= ( len h);

      i in ( dom h) by A2, A3, FINSEQ_3: 25;

      then (h /. i) in ( L~ h) by A1, GOBOARD1: 1, XXREAL_0: 2;

      hence thesis by PSCOMP_1: 24;

    end;

    theorem :: JORDAN5D:12

    

     Th12: 1 <= i & i <= ( len h) implies ( W-bound ( L~ h)) <= ((h /. i) `1 ) & ((h /. i) `1 ) <= ( E-bound ( L~ h))

    proof

      

       A1: ( len h) > 4 by GOBOARD7: 34;

      assume that

       A2: 1 <= i and

       A3: i <= ( len h);

      i in ( dom h) by A2, A3, FINSEQ_3: 25;

      then (h /. i) in ( L~ h) by A1, GOBOARD1: 1, XXREAL_0: 2;

      hence thesis by PSCOMP_1: 24;

    end;

    theorem :: JORDAN5D:13

    

     Th13: for X be Subset of REAL st X = { (q `2 ) : (q `1 ) = ( W-bound ( L~ h)) & q in ( L~ h) } holds X = (( proj2 | ( W-most ( L~ h))) .: the carrier of (( TOP-REAL 2) | ( W-most ( L~ h))))

    proof

      set T = (( TOP-REAL 2) | ( W-most ( L~ h)));

      set F = ( proj2 | ( W-most ( L~ h)));

      let X be Subset of REAL such that

       A1: X = { (q `2 ) : (q `1 ) = ( W-bound ( L~ h)) & q in ( L~ h) };

      thus X c= (( proj2 | ( W-most ( L~ h))) .: the carrier of T)

      proof

        let x be object;

        

         A2: ( dom F) = the carrier of T by FUNCT_2:def 1

        .= ( [#] (( TOP-REAL 2) | ( W-most ( L~ h))))

        .= ( W-most ( L~ h)) by PRE_TOPC:def 5;

        assume x in X;

        then

        consider q1 be Point of ( TOP-REAL 2) such that

         A3: (q1 `2 ) = x and

         A4: (q1 `1 ) = ( W-bound ( L~ h)) and

         A5: q1 in ( L~ h) by A1;

        

         A6: x = (F . q1) by A3, A4, A5, PSCOMP_1: 23, SPRECT_2: 12;

        

         A7: q1 in ( W-most ( L~ h)) by A4, A5, SPRECT_2: 12;

        then q1 in the carrier of T by A2, FUNCT_2:def 1;

        hence thesis by A2, A7, A6, FUNCT_1:def 6;

      end;

      thus (( proj2 | ( W-most ( L~ h))) .: the carrier of T) c= X

      proof

        let x be object;

        

         A8: ( W-most ( L~ h)) c= ( L~ h) by XBOOLE_1: 17;

        assume x in (( proj2 | ( W-most ( L~ h))) .: the carrier of T);

        then

        consider x1 be object such that x1 in ( dom F) and

         A9: x1 in the carrier of T and

         A10: x = (F . x1) by FUNCT_1:def 6;

        x1 in ( [#] (( TOP-REAL 2) | ( W-most ( L~ h)))) by A9;

        then

         A11: x1 in ( W-most ( L~ h)) by PRE_TOPC:def 5;

        then

        reconsider x2 = x1 as Element of ( TOP-REAL 2);

        

         A12: (x2 `1 ) = (( W-min ( L~ h)) `1 ) by A11, PSCOMP_1: 31

        .= ( W-bound ( L~ h)) by EUCLID: 52;

        x = (x2 `2 ) by A10, A11, PSCOMP_1: 23;

        hence thesis by A1, A11, A12, A8;

      end;

    end;

    theorem :: JORDAN5D:14

    

     Th14: for X be Subset of REAL st X = { (q `2 ) : (q `1 ) = ( E-bound ( L~ h)) & q in ( L~ h) } holds X = (( proj2 | ( E-most ( L~ h))) .: the carrier of (( TOP-REAL 2) | ( E-most ( L~ h))))

    proof

      set T = (( TOP-REAL 2) | ( E-most ( L~ h)));

      set F = ( proj2 | ( E-most ( L~ h)));

      let X be Subset of REAL such that

       A1: X = { (q `2 ) : (q `1 ) = ( E-bound ( L~ h)) & q in ( L~ h) };

      thus X c= (( proj2 | ( E-most ( L~ h))) .: the carrier of T)

      proof

        let x be object;

        

         A2: ( dom F) = the carrier of T by FUNCT_2:def 1

        .= ( [#] (( TOP-REAL 2) | ( E-most ( L~ h))))

        .= ( E-most ( L~ h)) by PRE_TOPC:def 5;

        assume x in X;

        then

        consider q1 be Point of ( TOP-REAL 2) such that

         A3: (q1 `2 ) = x and

         A4: (q1 `1 ) = ( E-bound ( L~ h)) and

         A5: q1 in ( L~ h) by A1;

        

         A6: x = (F . q1) by A3, A4, A5, PSCOMP_1: 23, SPRECT_2: 13;

        

         A7: q1 in ( E-most ( L~ h)) by A4, A5, SPRECT_2: 13;

        then q1 in the carrier of T by A2, FUNCT_2:def 1;

        hence thesis by A2, A7, A6, FUNCT_1:def 6;

      end;

      thus (( proj2 | ( E-most ( L~ h))) .: the carrier of T) c= X

      proof

        let x be object;

        

         A8: ( E-most ( L~ h)) c= ( L~ h) by XBOOLE_1: 17;

        assume x in (( proj2 | ( E-most ( L~ h))) .: the carrier of T);

        then

        consider x1 be object such that x1 in ( dom F) and

         A9: x1 in the carrier of T and

         A10: x = (F . x1) by FUNCT_1:def 6;

        x1 in ( [#] (( TOP-REAL 2) | ( E-most ( L~ h)))) by A9;

        then

         A11: x1 in ( E-most ( L~ h)) by PRE_TOPC:def 5;

        then

        reconsider x2 = x1 as Element of ( TOP-REAL 2);

        

         A12: (x2 `1 ) = (( E-min ( L~ h)) `1 ) by A11, PSCOMP_1: 47

        .= ( E-bound ( L~ h)) by EUCLID: 52;

        x = (x2 `2 ) by A10, A11, PSCOMP_1: 23;

        hence thesis by A1, A11, A12, A8;

      end;

    end;

    theorem :: JORDAN5D:15

    

     Th15: for X be Subset of REAL st X = { (q `1 ) : (q `2 ) = ( N-bound ( L~ h)) & q in ( L~ h) } holds X = (( proj1 | ( N-most ( L~ h))) .: the carrier of (( TOP-REAL 2) | ( N-most ( L~ h))))

    proof

      set T = (( TOP-REAL 2) | ( N-most ( L~ h)));

      set F = ( proj1 | ( N-most ( L~ h)));

      let X be Subset of REAL such that

       A1: X = { (q `1 ) : (q `2 ) = ( N-bound ( L~ h)) & q in ( L~ h) };

      thus X c= (( proj1 | ( N-most ( L~ h))) .: the carrier of T)

      proof

        let x be object;

        

         A2: ( dom F) = the carrier of T by FUNCT_2:def 1

        .= ( [#] (( TOP-REAL 2) | ( N-most ( L~ h))))

        .= ( N-most ( L~ h)) by PRE_TOPC:def 5;

        assume x in X;

        then

        consider q1 be Point of ( TOP-REAL 2) such that

         A3: (q1 `1 ) = x and

         A4: (q1 `2 ) = ( N-bound ( L~ h)) and

         A5: q1 in ( L~ h) by A1;

        

         A6: x = (F . q1) by A3, A4, A5, PSCOMP_1: 22, SPRECT_2: 10;

        

         A7: q1 in ( N-most ( L~ h)) by A4, A5, SPRECT_2: 10;

        then q1 in the carrier of T by A2, FUNCT_2:def 1;

        hence thesis by A2, A7, A6, FUNCT_1:def 6;

      end;

      thus (( proj1 | ( N-most ( L~ h))) .: the carrier of T) c= X

      proof

        let x be object;

        

         A8: ( N-most ( L~ h)) c= ( L~ h) by XBOOLE_1: 17;

        assume x in (( proj1 | ( N-most ( L~ h))) .: the carrier of T);

        then

        consider x1 be object such that x1 in ( dom F) and

         A9: x1 in the carrier of T and

         A10: x = (F . x1) by FUNCT_1:def 6;

        x1 in ( [#] (( TOP-REAL 2) | ( N-most ( L~ h)))) by A9;

        then

         A11: x1 in ( N-most ( L~ h)) by PRE_TOPC:def 5;

        then

        reconsider x2 = x1 as Element of ( TOP-REAL 2);

        

         A12: (x2 `2 ) = (( N-min ( L~ h)) `2 ) by A11, PSCOMP_1: 39

        .= ( N-bound ( L~ h)) by EUCLID: 52;

        x = (x2 `1 ) by A10, A11, PSCOMP_1: 22;

        hence thesis by A1, A11, A12, A8;

      end;

    end;

    theorem :: JORDAN5D:16

    

     Th16: for X be Subset of REAL st X = { (q `1 ) : (q `2 ) = ( S-bound ( L~ h)) & q in ( L~ h) } holds X = (( proj1 | ( S-most ( L~ h))) .: the carrier of (( TOP-REAL 2) | ( S-most ( L~ h))))

    proof

      set T = (( TOP-REAL 2) | ( S-most ( L~ h)));

      set F = ( proj1 | ( S-most ( L~ h)));

      let X be Subset of REAL such that

       A1: X = { (q `1 ) : (q `2 ) = ( S-bound ( L~ h)) & q in ( L~ h) };

      thus X c= (( proj1 | ( S-most ( L~ h))) .: the carrier of T)

      proof

        let x be object;

        

         A2: ( dom F) = the carrier of T by FUNCT_2:def 1

        .= ( [#] (( TOP-REAL 2) | ( S-most ( L~ h))))

        .= ( S-most ( L~ h)) by PRE_TOPC:def 5;

        assume x in X;

        then

        consider q1 be Point of ( TOP-REAL 2) such that

         A3: (q1 `1 ) = x and

         A4: (q1 `2 ) = ( S-bound ( L~ h)) and

         A5: q1 in ( L~ h) by A1;

        

         A6: x = (F . q1) by A3, A4, A5, PSCOMP_1: 22, SPRECT_2: 11;

        

         A7: q1 in ( S-most ( L~ h)) by A4, A5, SPRECT_2: 11;

        then q1 in the carrier of T by A2, FUNCT_2:def 1;

        hence thesis by A2, A7, A6, FUNCT_1:def 6;

      end;

      thus (( proj1 | ( S-most ( L~ h))) .: the carrier of T) c= X

      proof

        let x be object;

        

         A8: ( S-most ( L~ h)) c= ( L~ h) by XBOOLE_1: 17;

        assume x in (( proj1 | ( S-most ( L~ h))) .: the carrier of T);

        then

        consider x1 be object such that x1 in ( dom F) and

         A9: x1 in the carrier of T and

         A10: x = (F . x1) by FUNCT_1:def 6;

        x1 in ( [#] (( TOP-REAL 2) | ( S-most ( L~ h)))) by A9;

        then

         A11: x1 in ( S-most ( L~ h)) by PRE_TOPC:def 5;

        then

        reconsider x2 = x1 as Element of ( TOP-REAL 2);

        

         A12: (x2 `2 ) = (( S-min ( L~ h)) `2 ) by A11, PSCOMP_1: 55

        .= ( S-bound ( L~ h)) by EUCLID: 52;

        x = (x2 `1 ) by A10, A11, PSCOMP_1: 22;

        hence thesis by A1, A11, A12, A8;

      end;

    end;

    theorem :: JORDAN5D:17

    

     Th17: for X be Subset of REAL st X = { (q `1 ) : q in ( L~ g) } holds X = (( proj1 | ( L~ g)) .: the carrier of (( TOP-REAL 2) | ( L~ g)))

    proof

      set T = (( TOP-REAL 2) | ( L~ g));

      set F = ( proj1 | ( L~ g));

      let X be Subset of REAL such that

       A1: X = { (q `1 ) : q in ( L~ g) };

      thus X c= (( proj1 | ( L~ g)) .: the carrier of T)

      proof

        let x be object;

        assume x in X;

        then

        consider q1 be Point of ( TOP-REAL 2) such that

         A2: (q1 `1 ) = x and

         A3: q1 in ( L~ g) by A1;

        

         A4: x = (F . q1) by A2, A3, PSCOMP_1: 22;

        

         A5: ( dom F) = the carrier of T by FUNCT_2:def 1

        .= ( [#] (( TOP-REAL 2) | ( L~ g)))

        .= ( L~ g) by PRE_TOPC:def 5;

        then q1 in the carrier of T by A3, FUNCT_2:def 1;

        hence thesis by A3, A5, A4, FUNCT_1:def 6;

      end;

      thus (( proj1 | ( L~ g)) .: the carrier of T) c= X

      proof

        let x be object;

        assume x in (( proj1 | ( L~ g)) .: the carrier of T);

        then

        consider x1 be object such that x1 in ( dom F) and

         A6: x1 in the carrier of T and

         A7: x = (F . x1) by FUNCT_1:def 6;

        x1 in ( [#] (( TOP-REAL 2) | ( L~ g))) by A6;

        then

         A8: x1 in ( L~ g) by PRE_TOPC:def 5;

        then

        reconsider x2 = x1 as Element of ( TOP-REAL 2);

        x = (x2 `1 ) by A7, A8, PSCOMP_1: 22;

        hence thesis by A1, A8;

      end;

    end;

    theorem :: JORDAN5D:18

    

     Th18: for X be Subset of REAL st X = { (q `2 ) : q in ( L~ g) } holds X = (( proj2 | ( L~ g)) .: the carrier of (( TOP-REAL 2) | ( L~ g)))

    proof

      set T = (( TOP-REAL 2) | ( L~ g));

      set F = ( proj2 | ( L~ g));

      let X be Subset of REAL such that

       A1: X = { (q `2 ) : q in ( L~ g) };

      thus X c= (( proj2 | ( L~ g)) .: the carrier of T)

      proof

        let x be object;

        assume x in X;

        then

        consider q1 be Point of ( TOP-REAL 2) such that

         A2: (q1 `2 ) = x and

         A3: q1 in ( L~ g) by A1;

        

         A4: x = (F . q1) by A2, A3, PSCOMP_1: 23;

        

         A5: ( dom F) = the carrier of T by FUNCT_2:def 1

        .= ( [#] (( TOP-REAL 2) | ( L~ g)))

        .= ( L~ g) by PRE_TOPC:def 5;

        then q1 in the carrier of T by A3, FUNCT_2:def 1;

        hence thesis by A3, A5, A4, FUNCT_1:def 6;

      end;

      thus (( proj2 | ( L~ g)) .: the carrier of T) c= X

      proof

        let x be object;

        assume x in (( proj2 | ( L~ g)) .: the carrier of T);

        then

        consider x1 be object such that x1 in ( dom F) and

         A6: x1 in the carrier of T and

         A7: x = (F . x1) by FUNCT_1:def 6;

        x1 in ( [#] (( TOP-REAL 2) | ( L~ g))) by A6;

        then

         A8: x1 in ( L~ g) by PRE_TOPC:def 5;

        then

        reconsider x2 = x1 as Element of ( TOP-REAL 2);

        x = (x2 `2 ) by A7, A8, PSCOMP_1: 23;

        hence thesis by A1, A8;

      end;

    end;

    theorem :: JORDAN5D:19

    for X be Subset of REAL st X = { (q `2 ) : (q `1 ) = ( W-bound ( L~ h)) & q in ( L~ h) } holds ( lower_bound X) = ( lower_bound ( proj2 | ( W-most ( L~ h)))) by Th13;

    theorem :: JORDAN5D:20

    for X be Subset of REAL st X = { (q `2 ) : (q `1 ) = ( W-bound ( L~ h)) & q in ( L~ h) } holds ( upper_bound X) = ( upper_bound ( proj2 | ( W-most ( L~ h)))) by Th13;

    theorem :: JORDAN5D:21

    for X be Subset of REAL st X = { (q `2 ) : (q `1 ) = ( E-bound ( L~ h)) & q in ( L~ h) } holds ( lower_bound X) = ( lower_bound ( proj2 | ( E-most ( L~ h)))) by Th14;

    theorem :: JORDAN5D:22

    for X be Subset of REAL st X = { (q `2 ) : (q `1 ) = ( E-bound ( L~ h)) & q in ( L~ h) } holds ( upper_bound X) = ( upper_bound ( proj2 | ( E-most ( L~ h)))) by Th14;

    theorem :: JORDAN5D:23

    for X be Subset of REAL st X = { (q `1 ) : q in ( L~ g) } holds ( lower_bound X) = ( lower_bound ( proj1 | ( L~ g))) by Th17;

    theorem :: JORDAN5D:24

    for X be Subset of REAL st X = { (q `1 ) : (q `2 ) = ( S-bound ( L~ h)) & q in ( L~ h) } holds ( lower_bound X) = ( lower_bound ( proj1 | ( S-most ( L~ h)))) by Th16;

    theorem :: JORDAN5D:25

    for X be Subset of REAL st X = { (q `1 ) : (q `2 ) = ( S-bound ( L~ h)) & q in ( L~ h) } holds ( upper_bound X) = ( upper_bound ( proj1 | ( S-most ( L~ h)))) by Th16;

    theorem :: JORDAN5D:26

    for X be Subset of REAL st X = { (q `1 ) : (q `2 ) = ( N-bound ( L~ h)) & q in ( L~ h) } holds ( lower_bound X) = ( lower_bound ( proj1 | ( N-most ( L~ h)))) by Th15;

    theorem :: JORDAN5D:27

    for X be Subset of REAL st X = { (q `1 ) : (q `2 ) = ( N-bound ( L~ h)) & q in ( L~ h) } holds ( upper_bound X) = ( upper_bound ( proj1 | ( N-most ( L~ h)))) by Th15;

    theorem :: JORDAN5D:28

    for X be Subset of REAL st X = { (q `2 ) : q in ( L~ g) } holds ( lower_bound X) = ( lower_bound ( proj2 | ( L~ g))) by Th18;

    theorem :: JORDAN5D:29

    for X be Subset of REAL st X = { (q `1 ) : q in ( L~ g) } holds ( upper_bound X) = ( upper_bound ( proj1 | ( L~ g))) by Th17;

    theorem :: JORDAN5D:30

    for X be Subset of REAL st X = { (q `2 ) : q in ( L~ g) } holds ( upper_bound X) = ( upper_bound ( proj2 | ( L~ g))) by Th18;

    theorem :: JORDAN5D:31

    

     Th31: p in ( L~ h) & 1 <= I & I <= ( width ( GoB h)) implies ((( GoB h) * (1,I)) `1 ) <= (p `1 )

    proof

      assume that

       A1: p in ( L~ h) and

       A2: 1 <= I and

       A3: I <= ( width ( GoB h));

      consider i such that

       A4: 1 <= i and

       A5: (i + 1) <= ( len h) and

       A6: p in ( LSeg ((h /. i),(h /. (i + 1)))) by A1, SPPOL_2: 14;

      i <= (i + 1) by NAT_1: 11;

      then i <= ( len h) by A5, XXREAL_0: 2;

      then

       A7: ((( GoB h) * (1,I)) `1 ) <= ((h /. i) `1 ) by A2, A3, A4, Th5;

      1 <= (i + 1) by NAT_1: 11;

      then

       A8: ((( GoB h) * (1,I)) `1 ) <= ((h /. (i + 1)) `1 ) by A2, A3, A5, Th5;

      now

        per cases ;

          case ((h /. i) `1 ) <= ((h /. (i + 1)) `1 );

          then ((h /. i) `1 ) <= (p `1 ) by A6, TOPREAL1: 3;

          hence thesis by A7, XXREAL_0: 2;

        end;

          case ((h /. i) `1 ) > ((h /. (i + 1)) `1 );

          then ((h /. (i + 1)) `1 ) <= (p `1 ) by A6, TOPREAL1: 3;

          hence thesis by A8, XXREAL_0: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN5D:32

    

     Th32: p in ( L~ h) & 1 <= I & I <= ( width ( GoB h)) implies (p `1 ) <= ((( GoB h) * (( len ( GoB h)),I)) `1 )

    proof

      assume that

       A1: p in ( L~ h) and

       A2: 1 <= I and

       A3: I <= ( width ( GoB h));

      consider i such that

       A4: 1 <= i and

       A5: (i + 1) <= ( len h) and

       A6: p in ( LSeg ((h /. i),(h /. (i + 1)))) by A1, SPPOL_2: 14;

      i <= (i + 1) by NAT_1: 11;

      then i <= ( len h) by A5, XXREAL_0: 2;

      then

       A7: ((( GoB h) * (( len ( GoB h)),I)) `1 ) >= ((h /. i) `1 ) by A2, A3, A4, Th5;

      1 <= (i + 1) by NAT_1: 11;

      then

       A8: ((( GoB h) * (( len ( GoB h)),I)) `1 ) >= ((h /. (i + 1)) `1 ) by A2, A3, A5, Th5;

      now

        per cases ;

          case ((h /. i) `1 ) <= ((h /. (i + 1)) `1 );

          then ((h /. (i + 1)) `1 ) >= (p `1 ) by A6, TOPREAL1: 3;

          hence thesis by A8, XXREAL_0: 2;

        end;

          case ((h /. i) `1 ) > ((h /. (i + 1)) `1 );

          then ((h /. i) `1 ) >= (p `1 ) by A6, TOPREAL1: 3;

          hence thesis by A7, XXREAL_0: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN5D:33

    

     Th33: p in ( L~ h) & 1 <= I & I <= ( len ( GoB h)) implies ((( GoB h) * (I,1)) `2 ) <= (p `2 )

    proof

      assume that

       A1: p in ( L~ h) and

       A2: 1 <= I and

       A3: I <= ( len ( GoB h));

      consider i such that

       A4: 1 <= i and

       A5: (i + 1) <= ( len h) and

       A6: p in ( LSeg ((h /. i),(h /. (i + 1)))) by A1, SPPOL_2: 14;

      i <= (i + 1) by NAT_1: 11;

      then i <= ( len h) by A5, XXREAL_0: 2;

      then

       A7: ((( GoB h) * (I,1)) `2 ) <= ((h /. i) `2 ) by A2, A3, A4, Th6;

      1 <= (i + 1) by NAT_1: 11;

      then

       A8: ((( GoB h) * (I,1)) `2 ) <= ((h /. (i + 1)) `2 ) by A2, A3, A5, Th6;

      now

        per cases ;

          case ((h /. i) `2 ) <= ((h /. (i + 1)) `2 );

          then ((h /. i) `2 ) <= (p `2 ) by A6, TOPREAL1: 4;

          hence thesis by A7, XXREAL_0: 2;

        end;

          case ((h /. i) `2 ) > ((h /. (i + 1)) `2 );

          then ((h /. (i + 1)) `2 ) <= (p `2 ) by A6, TOPREAL1: 4;

          hence thesis by A8, XXREAL_0: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN5D:34

    

     Th34: p in ( L~ h) & 1 <= I & I <= ( len ( GoB h)) implies (p `2 ) <= ((( GoB h) * (I,( width ( GoB h)))) `2 )

    proof

      assume that

       A1: p in ( L~ h) and

       A2: 1 <= I and

       A3: I <= ( len ( GoB h));

      consider i such that

       A4: 1 <= i and

       A5: (i + 1) <= ( len h) and

       A6: p in ( LSeg ((h /. i),(h /. (i + 1)))) by A1, SPPOL_2: 14;

      i <= (i + 1) by NAT_1: 11;

      then i <= ( len h) by A5, XXREAL_0: 2;

      then

       A7: ((( GoB h) * (I,( width ( GoB h)))) `2 ) >= ((h /. i) `2 ) by A2, A3, A4, Th6;

      1 <= (i + 1) by NAT_1: 11;

      then

       A8: ((( GoB h) * (I,( width ( GoB h)))) `2 ) >= ((h /. (i + 1)) `2 ) by A2, A3, A5, Th6;

      now

        per cases ;

          case ((h /. i) `2 ) <= ((h /. (i + 1)) `2 );

          then ((h /. (i + 1)) `2 ) >= (p `2 ) by A6, TOPREAL1: 4;

          hence thesis by A8, XXREAL_0: 2;

        end;

          case ((h /. i) `2 ) > ((h /. (i + 1)) `2 );

          then ((h /. i) `2 ) >= (p `2 ) by A6, TOPREAL1: 4;

          hence thesis by A7, XXREAL_0: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: JORDAN5D:35

    

     Th35: 1 <= i & i <= ( len ( GoB h)) & 1 <= j & j <= ( width ( GoB h)) implies ex q st (q `1 ) = ((( GoB h) * (i,j)) `1 ) & q in ( L~ h)

    proof

      assume that

       A1: 1 <= i and

       A2: i <= ( len ( GoB h)) and

       A3: 1 <= j and

       A4: j <= ( width ( GoB h));

      consider k such that

       A5: k in ( dom h) and [i, j] in ( Indices ( GoB h)) and

       A6: ((h /. k) `1 ) = ((( GoB h) * (i,j)) `1 ) by A1, A2, A3, A4, Th9;

      take q = (h /. k);

      thus (q `1 ) = ((( GoB h) * (i,j)) `1 ) by A6;

      4 < ( len h) by GOBOARD7: 34;

      hence thesis by A5, GOBOARD1: 1, XXREAL_0: 2;

    end;

    theorem :: JORDAN5D:36

    

     Th36: 1 <= i & i <= ( len ( GoB h)) & 1 <= j & j <= ( width ( GoB h)) implies ex q st (q `2 ) = ((( GoB h) * (i,j)) `2 ) & q in ( L~ h)

    proof

      assume that

       A1: 1 <= i and

       A2: i <= ( len ( GoB h)) and

       A3: 1 <= j and

       A4: j <= ( width ( GoB h));

      consider k such that

       A5: k in ( dom h) and [i, j] in ( Indices ( GoB h)) and

       A6: ((h /. k) `2 ) = ((( GoB h) * (i,j)) `2 ) by A1, A2, A3, A4, Th10;

      take q = (h /. k);

      thus (q `2 ) = ((( GoB h) * (i,j)) `2 ) by A6;

      4 < ( len h) by GOBOARD7: 34;

      hence thesis by A5, GOBOARD1: 1, XXREAL_0: 2;

    end;

    theorem :: JORDAN5D:37

    

     Th37: ( W-bound ( L~ h)) = ((( GoB h) * (1,1)) `1 )

    proof

      set X = { (q `1 ) : q in ( L~ h) }, A = ((( GoB h) * (1,1)) `1 );

      consider a be object such that

       A1: a in ( L~ h) by XBOOLE_0:def 1;

      

       A2: X c= REAL

      proof

        let b be object;

        assume b in X;

        then ex qq be Point of ( TOP-REAL 2) st b = (qq `1 ) & qq in ( L~ h);

        hence thesis by XREAL_0:def 1;

      end;

      reconsider a as Point of ( TOP-REAL 2) by A1;

      (a `1 ) in X by A1;

      then

      reconsider X as non empty Subset of REAL by A2;

      ( lower_bound X) = A

      proof

        

         A3: 1 <= ( width ( GoB h)) by GOBOARD7: 33;

        

         A4: for p be Real st p in X holds p >= A

        proof

          let p be Real;

          assume p in X;

          then ex s be Point of ( TOP-REAL 2) st p = (s `1 ) & s in ( L~ h);

          hence thesis by A3, Th31;

        end;

        1 <= ( len ( GoB h)) by GOBOARD7: 32;

        then

        consider q1 be Point of ( TOP-REAL 2) such that

         A5: (q1 `1 ) = ((( GoB h) * (1,1)) `1 ) and

         A6: q1 in ( L~ h) by A3, Th35;

        reconsider q11 = (q1 `1 ) as Real;

        for q be Real st for p be Real st p in X holds p >= q holds A >= q

        proof

          

           A7: q11 in X by A6;

          let q be Real;

          assume for p be Real st p in X holds p >= q;

          hence thesis by A5, A7;

        end;

        hence thesis by A4, SEQ_4: 44;

      end;

      hence thesis by Th17;

    end;

    theorem :: JORDAN5D:38

    

     Th38: ( S-bound ( L~ h)) = ((( GoB h) * (1,1)) `2 )

    proof

      set X = { (q `2 ) : q in ( L~ h) }, A = ((( GoB h) * (1,1)) `2 );

      consider a be object such that

       A1: a in ( L~ h) by XBOOLE_0:def 1;

      

       A2: X c= REAL

      proof

        let b be object;

        assume b in X;

        then ex qq be Point of ( TOP-REAL 2) st b = (qq `2 ) & qq in ( L~ h);

        hence thesis by XREAL_0:def 1;

      end;

      reconsider a as Point of ( TOP-REAL 2) by A1;

      (a `2 ) in X by A1;

      then

      reconsider X as non empty Subset of REAL by A2;

      ( lower_bound X) = A

      proof

        

         A3: 1 <= ( len ( GoB h)) by GOBOARD7: 32;

        

         A4: for p be Real st p in X holds p >= A

        proof

          let p be Real;

          assume p in X;

          then ex s be Point of ( TOP-REAL 2) st p = (s `2 ) & s in ( L~ h);

          hence thesis by A3, Th33;

        end;

        1 <= ( width ( GoB h)) by GOBOARD7: 33;

        then

        consider q1 be Point of ( TOP-REAL 2) such that

         A5: (q1 `2 ) = ((( GoB h) * (1,1)) `2 ) and

         A6: q1 in ( L~ h) by A3, Th36;

        reconsider q11 = (q1 `2 ) as Real;

        for q be Real st for p be Real st p in X holds p >= q holds A >= q

        proof

          

           A7: q11 in X by A6;

          let q be Real;

          assume for p be Real st p in X holds p >= q;

          hence thesis by A5, A7;

        end;

        hence thesis by A4, SEQ_4: 44;

      end;

      hence thesis by Th18;

    end;

    theorem :: JORDAN5D:39

    

     Th39: ( E-bound ( L~ h)) = ((( GoB h) * (( len ( GoB h)),1)) `1 )

    proof

      set X = { (q `1 ) : q in ( L~ h) }, A = ((( GoB h) * (( len ( GoB h)),1)) `1 );

      consider a be object such that

       A1: a in ( L~ h) by XBOOLE_0:def 1;

      

       A2: X c= REAL

      proof

        let b be object;

        assume b in X;

        then ex qq be Point of ( TOP-REAL 2) st b = (qq `1 ) & qq in ( L~ h);

        hence thesis by XREAL_0:def 1;

      end;

      reconsider a as Point of ( TOP-REAL 2) by A1;

      (a `1 ) in X by A1;

      then

      reconsider X as non empty Subset of REAL by A2;

      ( upper_bound X) = A

      proof

        

         A3: for p be Real st p in X holds p <= A

        proof

          let p be Real;

          assume p in X;

          then

           A4: ex s be Point of ( TOP-REAL 2) st p = (s `1 ) & s in ( L~ h);

          1 <= ( width ( GoB h)) by GOBOARD7: 33;

          hence thesis by A4, Th32;

        end;

        

         A5: 1 <= ( width ( GoB h)) by GOBOARD7: 33;

        1 <= ( len ( GoB h)) by GOBOARD7: 32;

        then

        consider q1 be Point of ( TOP-REAL 2) such that

         A6: (q1 `1 ) = ((( GoB h) * (( len ( GoB h)),1)) `1 ) and

         A7: q1 in ( L~ h) by A5, Th35;

        reconsider q11 = (q1 `1 ) as Real;

        for q be Real st for p be Real st p in X holds p <= q holds A <= q

        proof

          

           A8: q11 in X by A7;

          let q be Real;

          assume for p be Real st p in X holds p <= q;

          hence thesis by A6, A8;

        end;

        hence thesis by A3, SEQ_4: 46;

      end;

      hence thesis by Th17;

    end;

    theorem :: JORDAN5D:40

    

     Th40: ( N-bound ( L~ h)) = ((( GoB h) * (1,( width ( GoB h)))) `2 )

    proof

      set X = { (q `2 ) : q in ( L~ h) }, A = ((( GoB h) * (1,( width ( GoB h)))) `2 );

      consider a be object such that

       A1: a in ( L~ h) by XBOOLE_0:def 1;

      

       A2: X c= REAL

      proof

        let b be object;

        assume b in X;

        then ex qq be Point of ( TOP-REAL 2) st b = (qq `2 ) & qq in ( L~ h);

        hence thesis by XREAL_0:def 1;

      end;

      reconsider a as Point of ( TOP-REAL 2) by A1;

      (a `2 ) in X by A1;

      then

      reconsider X as non empty Subset of REAL by A2;

      ( upper_bound X) = A

      proof

        

         A3: 1 <= ( len ( GoB h)) by GOBOARD7: 32;

        

         A4: for p be Real st p in X holds p <= A

        proof

          let p be Real;

          assume p in X;

          then ex s be Point of ( TOP-REAL 2) st p = (s `2 ) & s in ( L~ h);

          hence thesis by A3, Th34;

        end;

        1 <= ( width ( GoB h)) by GOBOARD7: 33;

        then

        consider q1 be Point of ( TOP-REAL 2) such that

         A5: (q1 `2 ) = ((( GoB h) * (1,( width ( GoB h)))) `2 ) and

         A6: q1 in ( L~ h) by A3, Th36;

        reconsider q11 = (q1 `2 ) as Real;

        for q be Real st for p be Real st p in X holds p <= q holds A <= q

        proof

          

           A7: q11 in X by A6;

          let q be Real;

          assume for p be Real st p in X holds p <= q;

          hence thesis by A5, A7;

        end;

        hence thesis by A4, SEQ_4: 46;

      end;

      hence thesis by Th18;

    end;

    theorem :: JORDAN5D:41

    

     Th41: for Y be non empty finite Subset of NAT st 1 <= i & i <= ( len f) & 1 <= I & I <= ( len ( GoB f)) & Y = { j where j be Element of NAT : [I, j] in ( Indices ( GoB f)) & ex k st k in ( dom f) & (f /. k) = (( GoB f) * (I,j)) } & ((f /. i) `1 ) = ((( GoB f) * (I,1)) `1 ) & i1 = ( min Y) holds ((( GoB f) * (I,i1)) `2 ) <= ((f /. i) `2 )

    proof

      let Y be non empty finite Subset of NAT ;

      

       A1: (f /. i) = |[((f /. i) `1 ), ((f /. i) `2 )]| by EUCLID: 53;

      assume

       A2: 1 <= i & i <= ( len f) & 1 <= I & I <= ( len ( GoB f)) & Y = { j where j be Element of NAT : [I, j] in ( Indices ( GoB f)) & ex k st k in ( dom f) & (f /. k) = (( GoB f) * (I,j)) } & ((f /. i) `1 ) = ((( GoB f) * (I,1)) `1 ) & i1 = ( min Y);

      then

       A3: i in ( dom f) by FINSEQ_3: 25;

      then

      consider i2,j2 be Nat such that

       A4: [i2, j2] in ( Indices ( GoB f)) and

       A5: (f /. i) = (( GoB f) * (i2,j2)) by GOBOARD5: 11;

      

       A6: j2 <= ( width ( GoB f)) by A4, MATRIX_0: 32;

      

       A7: 1 <= j2 by A4, MATRIX_0: 32;

      then

       A8: [I, j2] in ( Indices ( GoB f)) by A2, A6, MATRIX_0: 30;

      

       A9: i2 <= ( len ( GoB f)) by A4, MATRIX_0: 32;

      1 <= i2 by A4, MATRIX_0: 32;

      

      then

       A10: ((f /. i) `2 ) = ((( GoB f) * (1,j2)) `2 ) by A5, A9, A7, A6, GOBOARD5: 1

      .= ((( GoB f) * (I,j2)) `2 ) by A2, A7, A6, GOBOARD5: 1;

      i1 in Y by A2, XXREAL_2:def 7;

      then ex j be Element of NAT st i1 = j & [I, j] in ( Indices ( GoB f)) & ex k st k in ( dom f) & (f /. k) = (( GoB f) * (I,j)) by A2;

      then

       A11: 1 <= i1 by MATRIX_0: 32;

      

       A12: j2 in NAT by ORDINAL1:def 12;

      ((f /. i) `1 ) = ((( GoB f) * (I,j2)) `1 ) by A2, A7, A6, GOBOARD5: 2;

      then (f /. i) = (( GoB f) * (I,j2)) by A10, A1, EUCLID: 53;

      then j2 in Y by A2, A3, A8, A12;

      then

       A13: i1 <= j2 by A2, XXREAL_2:def 7;

      

       A14: j2 <= ( width ( GoB f)) by A4, MATRIX_0: 32;

      now

        per cases ;

          case i1 < j2;

          hence ((( GoB f) * (I,i1)) `2 ) <= ((( GoB f) * (I,j2)) `2 ) by A2, A11, A14, GOBOARD5: 4;

        end;

          case i1 >= j2;

          hence ((( GoB f) * (I,i1)) `2 ) <= ((( GoB f) * (I,j2)) `2 ) by A13, XXREAL_0: 1;

        end;

      end;

      hence thesis by A10;

    end;

    theorem :: JORDAN5D:42

    

     Th42: for Y be non empty finite Subset of NAT st 1 <= i & i <= ( len h) & 1 <= I & I <= ( width ( GoB h)) & Y = { j where j be Element of NAT : [j, I] in ( Indices ( GoB h)) & ex k st k in ( dom h) & (h /. k) = (( GoB h) * (j,I)) } & ((h /. i) `2 ) = ((( GoB h) * (1,I)) `2 ) & i1 = ( min Y) holds ((( GoB h) * (i1,I)) `1 ) <= ((h /. i) `1 )

    proof

      let Y be non empty finite Subset of NAT ;

      

       A1: (h /. i) = |[((h /. i) `1 ), ((h /. i) `2 )]| by EUCLID: 53;

      assume

       A2: 1 <= i & i <= ( len h) & 1 <= I & I <= ( width ( GoB h)) & Y = { j where j be Element of NAT : [j, I] in ( Indices ( GoB h)) & ex k st k in ( dom h) & (h /. k) = (( GoB h) * (j,I)) } & ((h /. i) `2 ) = ((( GoB h) * (1,I)) `2 ) & i1 = ( min Y);

      then

       A3: i in ( dom h) by FINSEQ_3: 25;

      then

      consider i2,j2 be Nat such that

       A4: [i2, j2] in ( Indices ( GoB h)) and

       A5: (h /. i) = (( GoB h) * (i2,j2)) by GOBOARD5: 11;

      

       A6: i2 <= ( len ( GoB h)) by A4, MATRIX_0: 32;

      

       A7: 1 <= i2 by A4, MATRIX_0: 32;

      then

       A8: [i2, I] in ( Indices ( GoB h)) by A2, A6, MATRIX_0: 30;

      

       A9: j2 <= ( width ( GoB h)) by A4, MATRIX_0: 32;

      1 <= j2 by A4, MATRIX_0: 32;

      

      then

       A10: ((h /. i) `1 ) = ((( GoB h) * (i2,1)) `1 ) by A5, A7, A6, A9, GOBOARD5: 2

      .= ((( GoB h) * (i2,I)) `1 ) by A2, A7, A6, GOBOARD5: 2;

      i1 in Y by A2, XXREAL_2:def 7;

      then ex j be Element of NAT st i1 = j & [j, I] in ( Indices ( GoB h)) & ex k st k in ( dom h) & (h /. k) = (( GoB h) * (j,I)) by A2;

      then

       A11: 1 <= i1 by MATRIX_0: 32;

      

       A12: i2 in NAT by ORDINAL1:def 12;

      ((h /. i) `2 ) = ((( GoB h) * (i2,I)) `2 ) by A2, A7, A6, GOBOARD5: 1;

      then (h /. i) = (( GoB h) * (i2,I)) by A10, A1, EUCLID: 53;

      then i2 in Y by A2, A3, A8, A12;

      then

       A13: i1 <= i2 by A2, XXREAL_2:def 7;

      

       A14: i2 <= ( len ( GoB h)) by A4, MATRIX_0: 32;

      now

        per cases ;

          case i1 < i2;

          hence ((( GoB h) * (i1,I)) `1 ) <= ((( GoB h) * (i2,I)) `1 ) by A2, A11, A14, GOBOARD5: 3;

        end;

          case i1 >= i2;

          hence ((( GoB h) * (i1,I)) `1 ) <= ((( GoB h) * (i2,I)) `1 ) by A13, XXREAL_0: 1;

        end;

      end;

      hence thesis by A10;

    end;

    theorem :: JORDAN5D:43

    

     Th43: for Y be non empty finite Subset of NAT st 1 <= i & i <= ( len h) & 1 <= I & I <= ( width ( GoB h)) & Y = { j where j be Element of NAT : [j, I] in ( Indices ( GoB h)) & ex k st k in ( dom h) & (h /. k) = (( GoB h) * (j,I)) } & ((h /. i) `2 ) = ((( GoB h) * (1,I)) `2 ) & i1 = ( max Y) holds ((( GoB h) * (i1,I)) `1 ) >= ((h /. i) `1 )

    proof

      let Y be non empty finite Subset of NAT ;

      

       A1: (h /. i) = |[((h /. i) `1 ), ((h /. i) `2 )]| by EUCLID: 53;

      assume

       A2: 1 <= i & i <= ( len h) & 1 <= I & I <= ( width ( GoB h)) & Y = { j where j be Element of NAT : [j, I] in ( Indices ( GoB h)) & ex k st k in ( dom h) & (h /. k) = (( GoB h) * (j,I)) } & ((h /. i) `2 ) = ((( GoB h) * (1,I)) `2 ) & i1 = ( max Y);

      then

       A3: i in ( dom h) by FINSEQ_3: 25;

      then

      consider i2,j2 be Nat such that

       A4: [i2, j2] in ( Indices ( GoB h)) and

       A5: (h /. i) = (( GoB h) * (i2,j2)) by GOBOARD5: 11;

      

       A6: 1 <= i2 by A4, MATRIX_0: 32;

      

       A7: i2 <= ( len ( GoB h)) by A4, MATRIX_0: 32;

      then

       A8: [i2, I] in ( Indices ( GoB h)) by A2, A6, MATRIX_0: 30;

      

       A9: j2 <= ( width ( GoB h)) by A4, MATRIX_0: 32;

      1 <= j2 by A4, MATRIX_0: 32;

      

      then

       A10: ((h /. i) `1 ) = ((( GoB h) * (i2,1)) `1 ) by A5, A6, A7, A9, GOBOARD5: 2

      .= ((( GoB h) * (i2,I)) `1 ) by A2, A6, A7, GOBOARD5: 2;

      i1 in Y by A2, XXREAL_2:def 8;

      then ex j be Element of NAT st i1 = j & [j, I] in ( Indices ( GoB h)) & ex k st k in ( dom h) & (h /. k) = (( GoB h) * (j,I)) by A2;

      then

       A11: i1 <= ( len ( GoB h)) by MATRIX_0: 32;

      

       A12: i2 in NAT by ORDINAL1:def 12;

      ((h /. i) `2 ) = ((( GoB h) * (i2,I)) `2 ) by A2, A6, A7, GOBOARD5: 1;

      then (h /. i) = (( GoB h) * (i2,I)) by A10, A1, EUCLID: 53;

      then i2 in Y by A2, A3, A8, A12;

      then

       A13: i1 >= i2 by A2, XXREAL_2:def 8;

      now

        per cases ;

          case i1 > i2;

          hence ((( GoB h) * (i1,I)) `1 ) >= ((( GoB h) * (i2,I)) `1 ) by A2, A6, A11, GOBOARD5: 3;

        end;

          case i1 <= i2;

          hence ((( GoB h) * (i1,I)) `1 ) >= ((( GoB h) * (i2,I)) `1 ) by A13, XXREAL_0: 1;

        end;

      end;

      hence thesis by A10;

    end;

    theorem :: JORDAN5D:44

    

     Th44: for Y be non empty finite Subset of NAT st 1 <= i & i <= ( len f) & 1 <= I & I <= ( len ( GoB f)) & Y = { j where j be Element of NAT : [I, j] in ( Indices ( GoB f)) & ex k st k in ( dom f) & (f /. k) = (( GoB f) * (I,j)) } & ((f /. i) `1 ) = ((( GoB f) * (I,1)) `1 ) & i1 = ( max Y) holds ((( GoB f) * (I,i1)) `2 ) >= ((f /. i) `2 )

    proof

      let Y be non empty finite Subset of NAT ;

      

       A1: (f /. i) = |[((f /. i) `1 ), ((f /. i) `2 )]| by EUCLID: 53;

      assume

       A2: 1 <= i & i <= ( len f) & 1 <= I & I <= ( len ( GoB f)) & Y = { j where j be Element of NAT : [I, j] in ( Indices ( GoB f)) & ex k st k in ( dom f) & (f /. k) = (( GoB f) * (I,j)) } & ((f /. i) `1 ) = ((( GoB f) * (I,1)) `1 ) & i1 = ( max Y);

      then

       A3: i in ( dom f) by FINSEQ_3: 25;

      then

      consider i2,j2 be Nat such that

       A4: [i2, j2] in ( Indices ( GoB f)) and

       A5: (f /. i) = (( GoB f) * (i2,j2)) by GOBOARD5: 11;

      

       A6: 1 <= j2 by A4, MATRIX_0: 32;

      

       A7: j2 <= ( width ( GoB f)) by A4, MATRIX_0: 32;

      then

       A8: [I, j2] in ( Indices ( GoB f)) by A2, A6, MATRIX_0: 30;

      

       A9: i2 <= ( len ( GoB f)) by A4, MATRIX_0: 32;

      1 <= i2 by A4, MATRIX_0: 32;

      

      then

       A10: ((f /. i) `2 ) = ((( GoB f) * (1,j2)) `2 ) by A5, A9, A6, A7, GOBOARD5: 1

      .= ((( GoB f) * (I,j2)) `2 ) by A2, A6, A7, GOBOARD5: 1;

      i1 in Y by A2, XXREAL_2:def 8;

      then ex j be Element of NAT st i1 = j & [I, j] in ( Indices ( GoB f)) & ex k st k in ( dom f) & (f /. k) = (( GoB f) * (I,j)) by A2;

      then

       A11: i1 <= ( width ( GoB f)) by MATRIX_0: 32;

      

       A12: j2 in NAT by ORDINAL1:def 12;

      ((f /. i) `1 ) = ((( GoB f) * (I,j2)) `1 ) by A2, A6, A7, GOBOARD5: 2;

      then (f /. i) = (( GoB f) * (I,j2)) by A10, A1, EUCLID: 53;

      then j2 in Y by A2, A3, A8, A12;

      then

       A13: i1 >= j2 by A2, XXREAL_2:def 8;

      now

        per cases ;

          case i1 > j2;

          hence ((( GoB f) * (I,i1)) `2 ) >= ((( GoB f) * (I,j2)) `2 ) by A2, A11, A6, GOBOARD5: 4;

        end;

          case i1 <= j2;

          hence ((( GoB f) * (I,i1)) `2 ) >= ((( GoB f) * (I,j2)) `2 ) by A13, XXREAL_0: 1;

        end;

      end;

      hence thesis by A10;

    end;

    

     Lm1: for p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT , h st (p `1 ) = ( W-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [1, j] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (1,j)) } & i1 = ( min Y) holds ((( GoB h) * (1,i1)) `2 ) <= (p `2 )

    proof

      let p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT , h;

      

       A1: 1 <= ( len ( GoB h)) by GOBOARD7: 32;

      assume

       A2: (p `1 ) = ( W-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [1, j] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (1,j)) } & i1 = ( min Y);

      then

      consider i such that

       A3: 1 <= i and

       A4: (i + 1) <= ( len h) and

       A5: p in ( LSeg ((h /. i),(h /. (i + 1)))) by SPPOL_2: 14;

      

       A6: 1 <= (i + 1) by A3, XREAL_1: 145;

      i <= (i + 1) by NAT_1: 11;

      then

       A7: i <= ( len h) by A4, XXREAL_0: 2;

      

       A8: (p `1 ) = ((( GoB h) * (1,1)) `1 ) by A2, Th37;

      

       A9: 1 <= ( width ( GoB h)) by GOBOARD7: 33;

      now

        per cases by SPPOL_1: 19;

          case ( LSeg (h,i)) is vertical;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is vertical by A3, A4, TOPREAL1:def 3;

          then

           A10: ((h /. i) `1 ) = ((h /. (i + 1)) `1 ) by SPPOL_1: 16;

          then

           A11: (p `1 ) = ((h /. i) `1 ) by A5, GOBOARD7: 5;

          

           A12: (p `1 ) = ((h /. (i + 1)) `1 ) by A5, A10, GOBOARD7: 5;

          now

            per cases ;

              case ((h /. i) `2 ) <= ((h /. (i + 1)) `2 );

              then

               A13: ((h /. i) `2 ) <= (p `2 ) by A5, TOPREAL1: 4;

              ((( GoB h) * (1,i1)) `2 ) <= ((h /. i) `2 ) by A2, A8, A1, A3, A7, A11, Th41;

              hence thesis by A13, XXREAL_0: 2;

            end;

              case ((h /. i) `2 ) > ((h /. (i + 1)) `2 );

              then

               A14: ((h /. (i + 1)) `2 ) <= (p `2 ) by A5, TOPREAL1: 4;

              ((( GoB h) * (1,i1)) `2 ) <= ((h /. (i + 1)) `2 ) by A2, A8, A1, A4, A6, A12, Th41;

              hence thesis by A14, XXREAL_0: 2;

            end;

          end;

          hence thesis;

        end;

          case ( LSeg (h,i)) is horizontal;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is horizontal by A3, A4, TOPREAL1:def 3;

          then

           A15: ((h /. i) `2 ) = ((h /. (i + 1)) `2 ) by SPPOL_1: 15;

          then

           A16: (p `2 ) = ((h /. i) `2 ) by A5, GOBOARD7: 6;

          

           A17: (p `2 ) = ((h /. (i + 1)) `2 ) by A5, A15, GOBOARD7: 6;

          now

            per cases ;

              case ((h /. i) `1 ) <= ((h /. (i + 1)) `1 );

              then

               A18: ((h /. i) `1 ) <= ((( GoB h) * (1,1)) `1 ) by A8, A5, TOPREAL1: 3;

              ((h /. i) `1 ) >= ((( GoB h) * (1,1)) `1 ) by A9, A3, A7, Th5;

              then ((h /. i) `1 ) = ((( GoB h) * (1,1)) `1 ) by A18, XXREAL_0: 1;

              hence thesis by A2, A1, A3, A7, A16, Th41;

            end;

              case ((h /. i) `1 ) > ((h /. (i + 1)) `1 );

              then

               A19: ((h /. (i + 1)) `1 ) <= ((( GoB h) * (1,1)) `1 ) by A8, A5, TOPREAL1: 3;

              ((h /. (i + 1)) `1 ) >= ((( GoB h) * (1,1)) `1 ) by A9, A4, A6, Th5;

              then ((h /. (i + 1)) `1 ) = ((( GoB h) * (1,1)) `1 ) by A19, XXREAL_0: 1;

              hence thesis by A2, A1, A4, A6, A17, Th41;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm2: for p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT , h st (p `1 ) = ( W-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [1, j] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (1,j)) } & i1 = ( max Y) holds ((( GoB h) * (1,i1)) `2 ) >= (p `2 )

    proof

      let p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT , h;

      

       A1: 1 <= ( len ( GoB h)) by GOBOARD7: 32;

      assume

       A2: (p `1 ) = ( W-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [1, j] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (1,j)) } & i1 = ( max Y);

      then

      consider i such that

       A3: 1 <= i and

       A4: (i + 1) <= ( len h) and

       A5: p in ( LSeg ((h /. i),(h /. (i + 1)))) by SPPOL_2: 14;

      

       A6: 1 <= (i + 1) by A3, XREAL_1: 145;

      i <= (i + 1) by NAT_1: 11;

      then

       A7: i <= ( len h) by A4, XXREAL_0: 2;

      

       A8: (p `1 ) = ((( GoB h) * (1,1)) `1 ) by A2, Th37;

      

       A9: 1 <= ( width ( GoB h)) by GOBOARD7: 33;

      now

        per cases by SPPOL_1: 19;

          case ( LSeg (h,i)) is vertical;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is vertical by A3, A4, TOPREAL1:def 3;

          then

           A10: ((h /. i) `1 ) = ((h /. (i + 1)) `1 ) by SPPOL_1: 16;

          then

           A11: (p `1 ) = ((h /. i) `1 ) by A5, GOBOARD7: 5;

          

           A12: (p `1 ) = ((h /. (i + 1)) `1 ) by A5, A10, GOBOARD7: 5;

          now

            per cases ;

              case ((h /. i) `2 ) >= ((h /. (i + 1)) `2 );

              then

               A13: ((h /. i) `2 ) >= (p `2 ) by A5, TOPREAL1: 4;

              ((( GoB h) * (1,i1)) `2 ) >= ((h /. i) `2 ) by A2, A8, A3, A1, A7, A11, Th44;

              hence thesis by A13, XXREAL_0: 2;

            end;

              case ((h /. i) `2 ) < ((h /. (i + 1)) `2 );

              then

               A14: ((h /. (i + 1)) `2 ) >= (p `2 ) by A5, TOPREAL1: 4;

              ((( GoB h) * (1,i1)) `2 ) >= ((h /. (i + 1)) `2 ) by A2, A8, A4, A1, A6, A12, Th44;

              hence thesis by A14, XXREAL_0: 2;

            end;

          end;

          hence thesis;

        end;

          case ( LSeg (h,i)) is horizontal;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is horizontal by A3, A4, TOPREAL1:def 3;

          then

           A15: ((h /. i) `2 ) = ((h /. (i + 1)) `2 ) by SPPOL_1: 15;

          then

           A16: (p `2 ) = ((h /. i) `2 ) by A5, GOBOARD7: 6;

          

           A17: (p `2 ) = ((h /. (i + 1)) `2 ) by A5, A15, GOBOARD7: 6;

          now

            per cases ;

              case ((h /. i) `1 ) <= ((h /. (i + 1)) `1 );

              then

               A18: ((h /. i) `1 ) <= ((( GoB h) * (1,1)) `1 ) by A8, A5, TOPREAL1: 3;

              ((h /. i) `1 ) >= ((( GoB h) * (1,1)) `1 ) by A3, A9, A7, Th5;

              then ((h /. i) `1 ) = ((( GoB h) * (1,1)) `1 ) by A18, XXREAL_0: 1;

              hence thesis by A2, A3, A1, A7, A16, Th44;

            end;

              case ((h /. i) `1 ) > ((h /. (i + 1)) `1 );

              then

               A19: ((h /. (i + 1)) `1 ) <= ((( GoB h) * (1,1)) `1 ) by A8, A5, TOPREAL1: 3;

              ((h /. (i + 1)) `1 ) >= ((( GoB h) * (1,1)) `1 ) by A4, A9, A6, Th5;

              then ((h /. (i + 1)) `1 ) = ((( GoB h) * (1,1)) `1 ) by A19, XXREAL_0: 1;

              hence thesis by A2, A4, A1, A6, A17, Th44;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm3: for p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT , h st (p `1 ) = ( E-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [( len ( GoB h)), j] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (( len ( GoB h)),j)) } & i1 = ( min Y) holds ((( GoB h) * (( len ( GoB h)),i1)) `2 ) <= (p `2 )

    proof

      let p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT , h;

      

       A1: 1 <= ( len ( GoB h)) by GOBOARD7: 32;

      assume

       A2: (p `1 ) = ( E-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [( len ( GoB h)), j] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (( len ( GoB h)),j)) } & i1 = ( min Y);

      then

      consider i such that

       A3: 1 <= i and

       A4: (i + 1) <= ( len h) and

       A5: p in ( LSeg ((h /. i),(h /. (i + 1)))) by SPPOL_2: 14;

      

       A6: 1 <= (i + 1) by A3, XREAL_1: 145;

      i <= (i + 1) by NAT_1: 11;

      then

       A7: i <= ( len h) by A4, XXREAL_0: 2;

      

       A8: (p `1 ) = ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A2, Th39;

      

       A9: 1 <= ( width ( GoB h)) by GOBOARD7: 33;

      now

        per cases by SPPOL_1: 19;

          case ( LSeg (h,i)) is vertical;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is vertical by A3, A4, TOPREAL1:def 3;

          then

           A10: ((h /. i) `1 ) = ((h /. (i + 1)) `1 ) by SPPOL_1: 16;

          then

           A11: (p `1 ) = ((h /. i) `1 ) by A5, GOBOARD7: 5;

          

           A12: (p `1 ) = ((h /. (i + 1)) `1 ) by A5, A10, GOBOARD7: 5;

          now

            per cases ;

              case ((h /. i) `2 ) <= ((h /. (i + 1)) `2 );

              then

               A13: ((h /. i) `2 ) <= (p `2 ) by A5, TOPREAL1: 4;

              ((( GoB h) * (( len ( GoB h)),i1)) `2 ) <= ((h /. i) `2 ) by A2, A8, A3, A7, A1, A11, Th41;

              hence thesis by A13, XXREAL_0: 2;

            end;

              case ((h /. i) `2 ) > ((h /. (i + 1)) `2 );

              then

               A14: ((h /. (i + 1)) `2 ) <= (p `2 ) by A5, TOPREAL1: 4;

              ((( GoB h) * (( len ( GoB h)),i1)) `2 ) <= ((h /. (i + 1)) `2 ) by A2, A8, A4, A6, A1, A12, Th41;

              hence thesis by A14, XXREAL_0: 2;

            end;

          end;

          hence thesis;

        end;

          case ( LSeg (h,i)) is horizontal;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is horizontal by A3, A4, TOPREAL1:def 3;

          then

           A15: ((h /. i) `2 ) = ((h /. (i + 1)) `2 ) by SPPOL_1: 15;

          then

           A16: (p `2 ) = ((h /. i) `2 ) by A5, GOBOARD7: 6;

          

           A17: (p `2 ) = ((h /. (i + 1)) `2 ) by A5, A15, GOBOARD7: 6;

          now

            per cases ;

              case ((h /. i) `1 ) >= ((h /. (i + 1)) `1 );

              then

               A18: ((h /. i) `1 ) >= ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A8, A5, TOPREAL1: 3;

              ((h /. i) `1 ) <= ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A9, A3, A7, Th5;

              then ((h /. i) `1 ) = ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A18, XXREAL_0: 1;

              hence thesis by A2, A3, A7, A1, A16, Th41;

            end;

              case ((h /. i) `1 ) < ((h /. (i + 1)) `1 );

              then

               A19: ((h /. (i + 1)) `1 ) >= ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A8, A5, TOPREAL1: 3;

              ((h /. (i + 1)) `1 ) <= ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A9, A4, A6, Th5;

              then ((h /. (i + 1)) `1 ) = ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A19, XXREAL_0: 1;

              hence thesis by A2, A4, A6, A1, A17, Th41;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm4: for p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT , h st (p `1 ) = ( E-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [( len ( GoB h)), j] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (( len ( GoB h)),j)) } & i1 = ( max Y) holds ((( GoB h) * (( len ( GoB h)),i1)) `2 ) >= (p `2 )

    proof

      let p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT , h;

      

       A1: 1 <= ( len ( GoB h)) by GOBOARD7: 32;

      assume

       A2: (p `1 ) = ( E-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [( len ( GoB h)), j] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (( len ( GoB h)),j)) } & i1 = ( max Y);

      then

      consider i such that

       A3: 1 <= i and

       A4: (i + 1) <= ( len h) and

       A5: p in ( LSeg ((h /. i),(h /. (i + 1)))) by SPPOL_2: 14;

      

       A6: 1 <= (i + 1) by A3, XREAL_1: 145;

      i <= (i + 1) by NAT_1: 11;

      then

       A7: i <= ( len h) by A4, XXREAL_0: 2;

      

       A8: (p `1 ) = ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A2, Th39;

      

       A9: 1 <= ( width ( GoB h)) by GOBOARD7: 33;

      now

        per cases by SPPOL_1: 19;

          case ( LSeg (h,i)) is vertical;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is vertical by A3, A4, TOPREAL1:def 3;

          then

           A10: ((h /. i) `1 ) = ((h /. (i + 1)) `1 ) by SPPOL_1: 16;

          then

           A11: (p `1 ) = ((h /. i) `1 ) by A5, GOBOARD7: 5;

          

           A12: (p `1 ) = ((h /. (i + 1)) `1 ) by A5, A10, GOBOARD7: 5;

          per cases ;

            suppose ((h /. i) `2 ) >= ((h /. (i + 1)) `2 );

            then

             A13: ((h /. i) `2 ) >= (p `2 ) by A5, TOPREAL1: 4;

            ((( GoB h) * (( len ( GoB h)),i1)) `2 ) >= ((h /. i) `2 ) by A2, A8, A1, A3, A7, A11, Th44;

            hence thesis by A13, XXREAL_0: 2;

          end;

            suppose ((h /. i) `2 ) < ((h /. (i + 1)) `2 );

            then

             A14: ((h /. (i + 1)) `2 ) >= (p `2 ) by A5, TOPREAL1: 4;

            ((( GoB h) * (( len ( GoB h)),i1)) `2 ) >= ((h /. (i + 1)) `2 ) by A2, A8, A1, A4, A6, A12, Th44;

            hence thesis by A14, XXREAL_0: 2;

          end;

        end;

          case ( LSeg (h,i)) is horizontal;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is horizontal by A3, A4, TOPREAL1:def 3;

          then

           A15: ((h /. i) `2 ) = ((h /. (i + 1)) `2 ) by SPPOL_1: 15;

          then

           A16: (p `2 ) = ((h /. i) `2 ) by A5, GOBOARD7: 6;

          

           A17: (p `2 ) = ((h /. (i + 1)) `2 ) by A5, A15, GOBOARD7: 6;

          now

            per cases ;

              case ((h /. i) `1 ) >= ((h /. (i + 1)) `1 );

              then

               A18: ((h /. i) `1 ) >= ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A8, A5, TOPREAL1: 3;

              ((h /. i) `1 ) <= ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A9, A3, A7, Th5;

              then ((h /. i) `1 ) = ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A18, XXREAL_0: 1;

              hence thesis by A2, A1, A3, A7, A16, Th44;

            end;

              case ((h /. i) `1 ) < ((h /. (i + 1)) `1 );

              then

               A19: ((h /. (i + 1)) `1 ) >= ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A8, A5, TOPREAL1: 3;

              ((h /. (i + 1)) `1 ) <= ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A9, A4, A6, Th5;

              then ((h /. (i + 1)) `1 ) = ((( GoB h) * (( len ( GoB h)),1)) `1 ) by A19, XXREAL_0: 1;

              hence thesis by A2, A1, A4, A6, A17, Th44;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm5: for p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT , h st (p `2 ) = ( S-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [j, 1] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (j,1)) } & i1 = ( min Y) holds ((( GoB h) * (i1,1)) `1 ) <= (p `1 )

    proof

      let p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT , h;

      

       A1: 1 <= ( width ( GoB h)) by GOBOARD7: 33;

      assume

       A2: (p `2 ) = ( S-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [j, 1] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (j,1)) } & i1 = ( min Y);

      then

      consider i such that

       A3: 1 <= i and

       A4: (i + 1) <= ( len h) and

       A5: p in ( LSeg ((h /. i),(h /. (i + 1)))) by SPPOL_2: 14;

      

       A6: 1 <= (i + 1) by A3, XREAL_1: 145;

      i <= (i + 1) by NAT_1: 11;

      then

       A7: i <= ( len h) by A4, XXREAL_0: 2;

      

       A8: (p `2 ) = ((( GoB h) * (1,1)) `2 ) by A2, Th38;

      

       A9: 1 <= ( len ( GoB h)) by GOBOARD7: 32;

      now

        per cases by SPPOL_1: 19;

          case ( LSeg (h,i)) is horizontal;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is horizontal by A3, A4, TOPREAL1:def 3;

          then

           A10: ((h /. i) `2 ) = ((h /. (i + 1)) `2 ) by SPPOL_1: 15;

          then

           A11: (p `2 ) = ((h /. i) `2 ) by A5, GOBOARD7: 6;

          

           A12: (p `2 ) = ((h /. (i + 1)) `2 ) by A5, A10, GOBOARD7: 6;

          now

            per cases ;

              case ((h /. i) `1 ) <= ((h /. (i + 1)) `1 );

              then

               A13: ((h /. i) `1 ) <= (p `1 ) by A5, TOPREAL1: 3;

              ((( GoB h) * (i1,1)) `1 ) <= ((h /. i) `1 ) by A2, A8, A3, A7, A1, A11, Th42;

              hence thesis by A13, XXREAL_0: 2;

            end;

              case ((h /. i) `1 ) > ((h /. (i + 1)) `1 );

              then

               A14: ((h /. (i + 1)) `1 ) <= (p `1 ) by A5, TOPREAL1: 3;

              ((( GoB h) * (i1,1)) `1 ) <= ((h /. (i + 1)) `1 ) by A2, A8, A4, A1, A6, A12, Th42;

              hence thesis by A14, XXREAL_0: 2;

            end;

          end;

          hence thesis;

        end;

          case ( LSeg (h,i)) is vertical;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is vertical by A3, A4, TOPREAL1:def 3;

          then

           A15: ((h /. i) `1 ) = ((h /. (i + 1)) `1 ) by SPPOL_1: 16;

          then

           A16: (p `1 ) = ((h /. i) `1 ) by A5, GOBOARD7: 5;

          

           A17: (p `1 ) = ((h /. (i + 1)) `1 ) by A5, A15, GOBOARD7: 5;

          now

            per cases ;

              case ((h /. i) `2 ) <= ((h /. (i + 1)) `2 );

              then

               A18: ((h /. i) `2 ) <= ((( GoB h) * (1,1)) `2 ) by A8, A5, TOPREAL1: 4;

              ((h /. i) `2 ) >= ((( GoB h) * (1,1)) `2 ) by A3, A7, A9, Th6;

              then ((h /. i) `2 ) = ((( GoB h) * (1,1)) `2 ) by A18, XXREAL_0: 1;

              hence thesis by A2, A3, A7, A1, A16, Th42;

            end;

              case ((h /. i) `2 ) > ((h /. (i + 1)) `2 );

              then

               A19: ((h /. (i + 1)) `2 ) <= ((( GoB h) * (1,1)) `2 ) by A8, A5, TOPREAL1: 4;

              ((h /. (i + 1)) `2 ) >= ((( GoB h) * (1,1)) `2 ) by A4, A9, A6, Th6;

              then ((h /. (i + 1)) `2 ) = ((( GoB h) * (1,1)) `2 ) by A19, XXREAL_0: 1;

              hence thesis by A2, A4, A1, A6, A17, Th42;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm6: for p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT , h st (p `2 ) = ( N-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [j, ( width ( GoB h))] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (j,( width ( GoB h)))) } & i1 = ( min Y) holds ((( GoB h) * (i1,( width ( GoB h)))) `1 ) <= (p `1 )

    proof

      let p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT , h;

      set I = ( width ( GoB h));

      

       A1: 1 <= I by GOBOARD7: 33;

      assume

       A2: (p `2 ) = ( N-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [j, ( width ( GoB h))] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (j,( width ( GoB h)))) } & i1 = ( min Y);

      then

      consider i such that

       A3: 1 <= i and

       A4: (i + 1) <= ( len h) and

       A5: p in ( LSeg ((h /. i),(h /. (i + 1)))) by SPPOL_2: 14;

      

       A6: (p `2 ) = ((( GoB h) * (1,( width ( GoB h)))) `2 ) by A2, Th40;

      i <= (i + 1) by NAT_1: 11;

      then

       A7: i <= ( len h) by A4, XXREAL_0: 2;

      

       A8: 1 <= (i + 1) by A3, XREAL_1: 145;

      now

        per cases by SPPOL_1: 19;

          case ( LSeg (h,i)) is horizontal;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is horizontal by A3, A4, TOPREAL1:def 3;

          then

           A9: ((h /. i) `2 ) = ((h /. (i + 1)) `2 ) by SPPOL_1: 15;

          then

           A10: (p `2 ) = ((h /. i) `2 ) by A5, GOBOARD7: 6;

          

           A11: (p `2 ) = ((h /. (i + 1)) `2 ) by A5, A9, GOBOARD7: 6;

          now

            per cases ;

              case ((h /. i) `1 ) <= ((h /. (i + 1)) `1 );

              then

               A12: ((h /. i) `1 ) <= (p `1 ) by A5, TOPREAL1: 3;

              ((( GoB h) * (i1,I)) `1 ) <= ((h /. i) `1 ) by A2, A6, A1, A3, A7, A10, Th42;

              hence thesis by A12, XXREAL_0: 2;

            end;

              case ((h /. i) `1 ) > ((h /. (i + 1)) `1 );

              then

               A13: ((h /. (i + 1)) `1 ) <= (p `1 ) by A5, TOPREAL1: 3;

              ((( GoB h) * (i1,I)) `1 ) <= ((h /. (i + 1)) `1 ) by A2, A6, A1, A4, A8, A11, Th42;

              hence thesis by A13, XXREAL_0: 2;

            end;

          end;

          hence thesis;

        end;

          case ( LSeg (h,i)) is vertical;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is vertical by A3, A4, TOPREAL1:def 3;

          then

           A14: ((h /. i) `1 ) = ((h /. (i + 1)) `1 ) by SPPOL_1: 16;

          then

           A15: (p `1 ) = ((h /. i) `1 ) by A5, GOBOARD7: 5;

          

           A16: 1 <= ( len ( GoB h)) by GOBOARD7: 32;

          

           A17: (p `1 ) = ((h /. (i + 1)) `1 ) by A5, A14, GOBOARD7: 5;

          now

            per cases ;

              case ((h /. i) `2 ) >= ((h /. (i + 1)) `2 );

              then

               A18: ((h /. i) `2 ) >= ((( GoB h) * (1,I)) `2 ) by A6, A5, TOPREAL1: 4;

              ((h /. i) `2 ) <= ((( GoB h) * (1,I)) `2 ) by A3, A7, A16, Th6;

              then ((h /. i) `2 ) = ((( GoB h) * (1,I)) `2 ) by A18, XXREAL_0: 1;

              hence thesis by A2, A1, A3, A7, A15, Th42;

            end;

              case ((h /. i) `2 ) < ((h /. (i + 1)) `2 );

              then

               A19: ((h /. (i + 1)) `2 ) >= ((( GoB h) * (1,I)) `2 ) by A6, A5, TOPREAL1: 4;

              ((h /. (i + 1)) `2 ) <= ((( GoB h) * (1,I)) `2 ) by A4, A8, A16, Th6;

              then ((h /. (i + 1)) `2 ) = ((( GoB h) * (1,I)) `2 ) by A19, XXREAL_0: 1;

              hence thesis by A2, A1, A4, A8, A17, Th42;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm7: for p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT st (p `2 ) = ( S-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [j, 1] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (j,1)) } & i1 = ( max Y) holds ((( GoB h) * (i1,1)) `1 ) >= (p `1 )

    proof

      let p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT ;

      

       A1: 1 <= ( width ( GoB h)) by GOBOARD7: 33;

      assume

       A2: (p `2 ) = ( S-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [j, 1] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (j,1)) } & i1 = ( max Y);

      then

      consider i such that

       A3: 1 <= i and

       A4: (i + 1) <= ( len h) and

       A5: p in ( LSeg ((h /. i),(h /. (i + 1)))) by SPPOL_2: 14;

      

       A6: 1 <= (i + 1) by A3, XREAL_1: 145;

      i <= (i + 1) by NAT_1: 11;

      then

       A7: i <= ( len h) by A4, XXREAL_0: 2;

      

       A8: (p `2 ) = ((( GoB h) * (1,1)) `2 ) by A2, Th38;

      

       A9: 1 <= ( len ( GoB h)) by GOBOARD7: 32;

      now

        per cases by SPPOL_1: 19;

          case ( LSeg (h,i)) is horizontal;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is horizontal by A3, A4, TOPREAL1:def 3;

          then

           A10: ((h /. i) `2 ) = ((h /. (i + 1)) `2 ) by SPPOL_1: 15;

          then

           A11: (p `2 ) = ((h /. i) `2 ) by A5, GOBOARD7: 6;

          

           A12: (p `2 ) = ((h /. (i + 1)) `2 ) by A5, A10, GOBOARD7: 6;

          now

            per cases ;

              case ((h /. i) `1 ) >= ((h /. (i + 1)) `1 );

              then

               A13: ((h /. i) `1 ) >= (p `1 ) by A5, TOPREAL1: 3;

              ((( GoB h) * (i1,1)) `1 ) >= ((h /. i) `1 ) by A2, A8, A3, A7, A1, A11, Th43;

              hence thesis by A13, XXREAL_0: 2;

            end;

              case ((h /. i) `1 ) < ((h /. (i + 1)) `1 );

              then

               A14: ((h /. (i + 1)) `1 ) >= (p `1 ) by A5, TOPREAL1: 3;

              ((( GoB h) * (i1,1)) `1 ) >= ((h /. (i + 1)) `1 ) by A2, A8, A4, A1, A6, A12, Th43;

              hence thesis by A14, XXREAL_0: 2;

            end;

          end;

          hence thesis;

        end;

          case ( LSeg (h,i)) is vertical;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is vertical by A3, A4, TOPREAL1:def 3;

          then

           A15: ((h /. i) `1 ) = ((h /. (i + 1)) `1 ) by SPPOL_1: 16;

          then

           A16: (p `1 ) = ((h /. i) `1 ) by A5, GOBOARD7: 5;

          

           A17: (p `1 ) = ((h /. (i + 1)) `1 ) by A5, A15, GOBOARD7: 5;

          now

            per cases ;

              case ((h /. i) `2 ) <= ((h /. (i + 1)) `2 );

              then

               A18: ((h /. i) `2 ) <= ((( GoB h) * (1,1)) `2 ) by A8, A5, TOPREAL1: 4;

              ((h /. i) `2 ) >= ((( GoB h) * (1,1)) `2 ) by A3, A7, A9, Th6;

              then ((h /. i) `2 ) = ((( GoB h) * (1,1)) `2 ) by A18, XXREAL_0: 1;

              hence thesis by A2, A3, A7, A1, A16, Th43;

            end;

              case ((h /. i) `2 ) > ((h /. (i + 1)) `2 );

              then

               A19: ((h /. (i + 1)) `2 ) <= ((( GoB h) * (1,1)) `2 ) by A8, A5, TOPREAL1: 4;

              ((h /. (i + 1)) `2 ) >= ((( GoB h) * (1,1)) `2 ) by A4, A9, A6, Th6;

              then ((h /. (i + 1)) `2 ) = ((( GoB h) * (1,1)) `2 ) by A19, XXREAL_0: 1;

              hence thesis by A2, A4, A1, A6, A17, Th43;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm8: for p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT st (p `2 ) = ( N-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [j, ( width ( GoB h))] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (j,( width ( GoB h)))) } & i1 = ( max Y) holds ((( GoB h) * (i1,( width ( GoB h)))) `1 ) >= (p `1 )

    proof

      let p be Point of ( TOP-REAL 2), Y be non empty finite Subset of NAT ;

      assume

       A1: (p `2 ) = ( N-bound ( L~ h)) & p in ( L~ h) & Y = { j where j be Element of NAT : [j, ( width ( GoB h))] in ( Indices ( GoB h)) & ex i st i in ( dom h) & (h /. i) = (( GoB h) * (j,( width ( GoB h)))) } & i1 = ( max Y);

      then

      consider i such that

       A2: 1 <= i and

       A3: (i + 1) <= ( len h) and

       A4: p in ( LSeg ((h /. i),(h /. (i + 1)))) by SPPOL_2: 14;

      

       A5: (p `2 ) = ((( GoB h) * (1,( width ( GoB h)))) `2 ) by A1, Th40;

      i <= (i + 1) by NAT_1: 11;

      then

       A6: i <= ( len h) by A3, XXREAL_0: 2;

      

       A7: 1 <= (i + 1) by A2, XREAL_1: 145;

      now

        per cases by SPPOL_1: 19;

          case ( LSeg (h,i)) is horizontal;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is horizontal by A2, A3, TOPREAL1:def 3;

          then

           A8: ((h /. i) `2 ) = ((h /. (i + 1)) `2 ) by SPPOL_1: 15;

          then

           A9: (p `2 ) = ((h /. i) `2 ) by A4, GOBOARD7: 6;

          

           A10: (p `2 ) = ((h /. (i + 1)) `2 ) by A4, A8, GOBOARD7: 6;

          now

            per cases ;

              case

               A11: ((h /. i) `1 ) >= ((h /. (i + 1)) `1 );

              1 <= ( width ( GoB h)) by GOBOARD7: 33;

              then

               A12: ((( GoB h) * (i1,( width ( GoB h)))) `1 ) >= ((h /. i) `1 ) by A1, A5, A2, A6, A9, Th43;

              ((h /. i) `1 ) >= (p `1 ) by A4, A11, TOPREAL1: 3;

              hence thesis by A12, XXREAL_0: 2;

            end;

              case

               A13: ((h /. i) `1 ) < ((h /. (i + 1)) `1 );

              1 <= ( width ( GoB h)) by GOBOARD7: 33;

              then

               A14: ((( GoB h) * (i1,( width ( GoB h)))) `1 ) >= ((h /. (i + 1)) `1 ) by A1, A5, A3, A7, A10, Th43;

              ((h /. (i + 1)) `1 ) >= (p `1 ) by A4, A13, TOPREAL1: 3;

              hence thesis by A14, XXREAL_0: 2;

            end;

          end;

          hence thesis;

        end;

          case ( LSeg (h,i)) is vertical;

          then ( LSeg ((h /. i),(h /. (i + 1)))) is vertical by A2, A3, TOPREAL1:def 3;

          then

           A15: ((h /. i) `1 ) = ((h /. (i + 1)) `1 ) by SPPOL_1: 16;

          then

           A16: (p `1 ) = ((h /. i) `1 ) by A4, GOBOARD7: 5;

          

           A17: 1 <= ( len ( GoB h)) by GOBOARD7: 32;

          

           A18: (p `1 ) = ((h /. (i + 1)) `1 ) by A4, A15, GOBOARD7: 5;

          now

            per cases ;

              case ((h /. i) `2 ) >= ((h /. (i + 1)) `2 );

              then

               A19: ((h /. i) `2 ) >= ((( GoB h) * (1,( width ( GoB h)))) `2 ) by A5, A4, TOPREAL1: 4;

              ((h /. i) `2 ) <= ((( GoB h) * (1,( width ( GoB h)))) `2 ) by A2, A6, A17, Th6;

              then

               A20: ((h /. i) `2 ) = ((( GoB h) * (1,( width ( GoB h)))) `2 ) by A19, XXREAL_0: 1;

              1 <= ( width ( GoB h)) by GOBOARD7: 33;

              hence thesis by A1, A2, A6, A16, A20, Th43;

            end;

              case ((h /. i) `2 ) < ((h /. (i + 1)) `2 );

              then

               A21: ((h /. (i + 1)) `2 ) >= ((( GoB h) * (1,( width ( GoB h)))) `2 ) by A5, A4, TOPREAL1: 4;

              ((h /. (i + 1)) `2 ) <= ((( GoB h) * (1,( width ( GoB h)))) `2 ) by A3, A7, A17, Th6;

              then

               A22: ((h /. (i + 1)) `2 ) = ((( GoB h) * (1,( width ( GoB h)))) `2 ) by A21, XXREAL_0: 1;

              1 <= ( width ( GoB h)) by GOBOARD7: 33;

              hence thesis by A1, A3, A7, A18, A22, Th43;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm9: ( len h) >= 2 by GOBOARD7: 34, XXREAL_0: 2;

    begin

    definition

      let g be non constant standard special_circular_sequence;

      :: JORDAN5D:def1

      func i_s_w g -> Nat means

      : Def1: [1, it ] in ( Indices ( GoB g)) & (( GoB g) * (1,it )) = ( W-min ( L~ g));

      existence

      proof

        { (q `2 ) : (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g) } c= REAL

        proof

          let X be object;

          assume X in { (q `2 ) : (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g) };

          then ex q st X = (q `2 ) & (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g);

          hence thesis by XREAL_0:def 1;

        end;

        then

        reconsider B = { (q `2 ) : (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g) } as Subset of REAL ;

        set s1 = ((( GoB g) * (1,1)) `2 );

        defpred P[ Nat] means [1, $1] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * (1,$1));

        set Y = { j where j be Element of NAT : P[j] };

        

         A1: Y c= ( Seg ( width ( GoB g)))

        proof

          let y be object;

          assume y in Y;

          then ex j be Element of NAT st y = j & [1, j] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * (1,j));

          then [1, y] in [:( dom ( GoB g)), ( Seg ( width ( GoB g))):] by MATRIX_0:def 4;

          hence thesis by ZFMISC_1: 87;

        end;

        

         A2: Y is Subset of NAT from DOMAIN_1:sch 7;

        

         A3: 1 <= ( len ( GoB g)) by GOBOARD7: 32;

        then

        consider i, j such that

         A4: i in ( dom g) and

         A5: [1, j] in ( Indices ( GoB g)) and

         A6: (g /. i) = (( GoB g) * (1,j)) by Th7;

        j in NAT by ORDINAL1:def 12;

        then j in Y by A4, A5, A6;

        then

        reconsider Y as non empty finite Subset of NAT by A1, A2;

        set i1 = ( min Y);

        i1 in Y by XXREAL_2:def 7;

        then

        consider j be Element of NAT such that

         A7: j = i1 and

         A8: [1, j] in ( Indices ( GoB g)) and

         A9: ex i be Nat st i in ( dom g) & (g /. i) = (( GoB g) * (1,j));

        

         A10: i1 <= ( width ( GoB g)) by A7, A8, MATRIX_0: 32;

        

         A11: 1 <= ( len ( GoB g)) by A8, MATRIX_0: 32;

        1 <= i1 by A7, A8, MATRIX_0: 32;

        then

         A12: ((( GoB g) * (1,i1)) `1 ) = ((( GoB g) * (1,1)) `1 ) by A11, A10, GOBOARD5: 2;

        then

         A13: ((( GoB g) * (1,i1)) `1 ) = ( W-bound ( L~ g)) by Th37;

        consider i such that

         A14: i in ( dom g) and

         A15: (g /. i) = (( GoB g) * (1,j)) by A9;

        

         A16: i <= ( len g) by A14, FINSEQ_3: 25;

        

         A17: 1 <= i by A14, FINSEQ_3: 25;

         A18:

        now

          per cases by A16, XXREAL_0: 1;

            case i < ( len g);

            then (i + 1) <= ( len g) by NAT_1: 13;

            then (g /. i) in ( LSeg (g,i)) by A17, TOPREAL1: 21;

            hence (( GoB g) * (1,i1)) in ( L~ g) by A7, A15, SPPOL_2: 17;

          end;

            case i = ( len g);

            then (g /. i) in ( LSeg (g,(i -' 1))) by Lm9, Th1;

            hence (( GoB g) * (1,i1)) in ( L~ g) by A7, A15, SPPOL_2: 17;

          end;

        end;

        ((( GoB g) * (1,i1)) `1 ) = ( W-bound ( L~ g)) by A12, Th37;

        then

         A19: ((( GoB g) * (1,i1)) `2 ) in { (q `2 ) : (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g) } by A18;

        for r be Real st r in B holds r >= ((( GoB g) * (1,i1)) `2 )

        proof

          let r be Real;

          assume r in B;

          then ex q st r = (q `2 ) & (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g);

          hence thesis by Lm1;

        end;

        then

         A20: ( lower_bound B) >= ((( GoB g) * (1,i1)) `2 ) by A19, SEQ_4: 43;

        s1 is LowerBound of B

        proof

          let r be ExtReal;

          assume r in B;

          then ex q st r = (q `2 ) & (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g);

          hence thesis by A3, Th33;

        end;

        then B is bounded_below;

        then ( lower_bound B) <= ((( GoB g) * (1,i1)) `2 ) by A19, SEQ_4:def 2;

        

        then ((( GoB g) * (1,i1)) `2 ) = ( lower_bound B) by A20, XXREAL_0: 1

        .= ( lower_bound ( proj2 | ( W-most ( L~ g)))) by Th13;

        hence thesis by A7, A8, A13, EUCLID: 53;

      end;

      uniqueness by GOBOARD1: 5;

      :: JORDAN5D:def2

      func i_n_w g -> Nat means

      : Def2: [1, it ] in ( Indices ( GoB g)) & (( GoB g) * (1,it )) = ( W-max ( L~ g));

      existence

      proof

        { (q `2 ) : (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g) } c= REAL

        proof

          let X be object;

          assume X in { (q `2 ) : (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g) };

          then ex q st X = (q `2 ) & (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g);

          hence thesis by XREAL_0:def 1;

        end;

        then

        reconsider B = { (q `2 ) : (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g) } as Subset of REAL ;

        set s1 = ((( GoB g) * (1,( width ( GoB g)))) `2 );

        defpred P[ Nat] means [1, $1] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * (1,$1));

        set Y = { j where j be Element of NAT : P[j] };

        

         A21: Y c= ( Seg ( width ( GoB g)))

        proof

          let y be object;

          assume y in Y;

          then ex j be Element of NAT st y = j & [1, j] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * (1,j));

          then [1, y] in [:( dom ( GoB g)), ( Seg ( width ( GoB g))):] by MATRIX_0:def 4;

          hence thesis by ZFMISC_1: 87;

        end;

        

         A22: Y is Subset of NAT from DOMAIN_1:sch 7;

        

         A23: 1 <= ( len ( GoB g)) by GOBOARD7: 32;

        then

        consider i, j such that

         A24: i in ( dom g) and

         A25: [1, j] in ( Indices ( GoB g)) and

         A26: (g /. i) = (( GoB g) * (1,j)) by Th7;

        j in NAT by ORDINAL1:def 12;

        then j in Y by A24, A25, A26;

        then

        reconsider Y as non empty finite Subset of NAT by A21, A22;

        reconsider i1 = ( max Y) as Nat by TARSKI: 1;

        i1 in Y by XXREAL_2:def 8;

        then

        consider j be Element of NAT such that

         A27: j = i1 and

         A28: [1, j] in ( Indices ( GoB g)) and

         A29: ex i be Nat st i in ( dom g) & (g /. i) = (( GoB g) * (1,j));

        

         A30: i1 <= ( width ( GoB g)) by A27, A28, MATRIX_0: 32;

        

         A31: 1 <= ( len ( GoB g)) by A28, MATRIX_0: 32;

        1 <= i1 by A27, A28, MATRIX_0: 32;

        then

         A32: ((( GoB g) * (1,i1)) `1 ) = ((( GoB g) * (1,1)) `1 ) by A31, A30, GOBOARD5: 2;

        then

         A33: ((( GoB g) * (1,i1)) `1 ) = ( W-bound ( L~ g)) by Th37;

        consider i such that

         A34: i in ( dom g) and

         A35: (g /. i) = (( GoB g) * (1,j)) by A29;

        

         A36: i <= ( len g) by A34, FINSEQ_3: 25;

        

         A37: 1 <= i by A34, FINSEQ_3: 25;

         A38:

        now

          per cases by A36, XXREAL_0: 1;

            case i < ( len g);

            then (i + 1) <= ( len g) by NAT_1: 13;

            then (g /. i) in ( LSeg (g,i)) by A37, TOPREAL1: 21;

            hence (( GoB g) * (1,i1)) in ( L~ g) by A27, A35, SPPOL_2: 17;

          end;

            case i = ( len g);

            then (g /. i) in ( LSeg (g,(i -' 1))) by Lm9, Th1;

            hence (( GoB g) * (1,i1)) in ( L~ g) by A27, A35, SPPOL_2: 17;

          end;

        end;

        ((( GoB g) * (1,i1)) `1 ) = ( W-bound ( L~ g)) by A32, Th37;

        then

         A39: ((( GoB g) * (1,i1)) `2 ) in { (q `2 ) : (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g) } by A38;

        for r be Real st r in B holds r <= ((( GoB g) * (1,i1)) `2 )

        proof

          let r be Real;

          assume r in B;

          then ex q st r = (q `2 ) & (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g);

          hence thesis by Lm2;

        end;

        then

         A40: ( upper_bound B) <= ((( GoB g) * (1,i1)) `2 ) by A39, SEQ_4: 45;

        s1 is UpperBound of B

        proof

          let r be ExtReal;

          assume r in B;

          then ex q st r = (q `2 ) & (q `1 ) = ( W-bound ( L~ g)) & q in ( L~ g);

          hence thesis by A23, Th34;

        end;

        then B is bounded_above;

        then ( upper_bound B) >= ((( GoB g) * (1,i1)) `2 ) by A39, SEQ_4:def 1;

        

        then ((( GoB g) * (1,i1)) `2 ) = ( upper_bound B) by A40, XXREAL_0: 1

        .= ( upper_bound ( proj2 | ( W-most ( L~ g)))) by Th13;

        hence thesis by A27, A28, A33, EUCLID: 53;

      end;

      uniqueness by GOBOARD1: 5;

      :: JORDAN5D:def3

      func i_s_e g -> Nat means

      : Def3: [( len ( GoB g)), it ] in ( Indices ( GoB g)) & (( GoB g) * (( len ( GoB g)),it )) = ( E-min ( L~ g));

      existence

      proof

        { (q `2 ) : (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g) } c= REAL

        proof

          let X be object;

          assume X in { (q `2 ) : (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g) };

          then ex q st X = (q `2 ) & (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g);

          hence thesis by XREAL_0:def 1;

        end;

        then

        reconsider B = { (q `2 ) : (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g) } as Subset of REAL ;

        set s1 = ((( GoB g) * (( len ( GoB g)),1)) `2 );

        defpred P[ Nat] means [( len ( GoB g)), $1] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * (( len ( GoB g)),$1));

        set Y = { j where j be Element of NAT : P[j] };

        

         A41: Y c= ( Seg ( width ( GoB g)))

        proof

          let y be object;

          assume y in Y;

          then ex j be Element of NAT st y = j & [( len ( GoB g)), j] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * (( len ( GoB g)),j));

          then [( len ( GoB g)), y] in [:( dom ( GoB g)), ( Seg ( width ( GoB g))):] by MATRIX_0:def 4;

          hence thesis by ZFMISC_1: 87;

        end;

        

         A42: Y is Subset of NAT from DOMAIN_1:sch 7;

        

         A43: 1 <= ( len ( GoB g)) by GOBOARD7: 32;

        then

        consider i, j such that

         A44: i in ( dom g) and

         A45: [( len ( GoB g)), j] in ( Indices ( GoB g)) and

         A46: (g /. i) = (( GoB g) * (( len ( GoB g)),j)) by Th7;

        j in NAT by ORDINAL1:def 12;

        then j in Y by A44, A45, A46;

        then

        reconsider Y as non empty finite Subset of NAT by A41, A42;

        set i1 = ( min Y);

        i1 in Y by XXREAL_2:def 7;

        then

        consider j be Element of NAT such that

         A47: j = i1 and

         A48: [( len ( GoB g)), j] in ( Indices ( GoB g)) and

         A49: ex i st i in ( dom g) & (g /. i) = (( GoB g) * (( len ( GoB g)),j));

        

         A50: i1 <= ( width ( GoB g)) by A47, A48, MATRIX_0: 32;

        

         A51: 1 <= ( len ( GoB g)) by A48, MATRIX_0: 32;

        1 <= i1 by A47, A48, MATRIX_0: 32;

        then

         A52: ((( GoB g) * (( len ( GoB g)),i1)) `1 ) = ((( GoB g) * (( len ( GoB g)),1)) `1 ) by A51, A50, GOBOARD5: 2;

        then

         A53: ((( GoB g) * (( len ( GoB g)),i1)) `1 ) = ( E-bound ( L~ g)) by Th39;

        consider i such that

         A54: i in ( dom g) and

         A55: (g /. i) = (( GoB g) * (( len ( GoB g)),j)) by A49;

        

         A56: i <= ( len g) by A54, FINSEQ_3: 25;

        

         A57: 1 <= i by A54, FINSEQ_3: 25;

         A58:

        now

          per cases by A56, XXREAL_0: 1;

            case i < ( len g);

            then (i + 1) <= ( len g) by NAT_1: 13;

            then (g /. i) in ( LSeg (g,i)) by A57, TOPREAL1: 21;

            hence (( GoB g) * (( len ( GoB g)),i1)) in ( L~ g) by A47, A55, SPPOL_2: 17;

          end;

            case i = ( len g);

            then (g /. i) in ( LSeg (g,(i -' 1))) by Lm9, Th1;

            hence (( GoB g) * (( len ( GoB g)),i1)) in ( L~ g) by A47, A55, SPPOL_2: 17;

          end;

        end;

        ((( GoB g) * (( len ( GoB g)),i1)) `1 ) = ( E-bound ( L~ g)) by A52, Th39;

        then

         A59: ((( GoB g) * (( len ( GoB g)),i1)) `2 ) in { (q `2 ) : (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g) } by A58;

        for r be Real st r in B holds r >= ((( GoB g) * (( len ( GoB g)),i1)) `2 )

        proof

          let r be Real;

          assume r in B;

          then ex q st r = (q `2 ) & (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g);

          hence thesis by Lm3;

        end;

        then

         A60: ( lower_bound B) >= ((( GoB g) * (( len ( GoB g)),i1)) `2 ) by A59, SEQ_4: 43;

        s1 is LowerBound of B

        proof

          let r be ExtReal;

          assume r in B;

          then ex q st r = (q `2 ) & (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g);

          hence thesis by A43, Th33;

        end;

        then B is bounded_below;

        then ( lower_bound B) <= ((( GoB g) * (( len ( GoB g)),i1)) `2 ) by A59, SEQ_4:def 2;

        

        then ((( GoB g) * (( len ( GoB g)),i1)) `2 ) = ( lower_bound B) by A60, XXREAL_0: 1

        .= ( lower_bound ( proj2 | ( E-most ( L~ g)))) by Th14;

        hence thesis by A47, A48, A53, EUCLID: 53;

      end;

      uniqueness by GOBOARD1: 5;

      :: JORDAN5D:def4

      func i_n_e g -> Nat means

      : Def4: [( len ( GoB g)), it ] in ( Indices ( GoB g)) & (( GoB g) * (( len ( GoB g)),it )) = ( E-max ( L~ g));

      existence

      proof

        { (q `2 ) : (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g) } c= REAL

        proof

          let X be object;

          assume X in { (q `2 ) : (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g) };

          then ex q st X = (q `2 ) & (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g);

          hence thesis by XREAL_0:def 1;

        end;

        then

        reconsider B = { (q `2 ) : (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g) } as Subset of REAL ;

        defpred P[ Nat] means [( len ( GoB g)), $1] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * (( len ( GoB g)),$1));

        set Y = { j where j be Element of NAT : P[j] };

        

         A61: Y c= ( Seg ( width ( GoB g)))

        proof

          let y be object;

          assume y in Y;

          then ex j be Element of NAT st y = j & [( len ( GoB g)), j] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * (( len ( GoB g)),j));

          then [( len ( GoB g)), y] in [:( dom ( GoB g)), ( Seg ( width ( GoB g))):] by MATRIX_0:def 4;

          hence thesis by ZFMISC_1: 87;

        end;

        

         A62: Y is Subset of NAT from DOMAIN_1:sch 7;

         0 <> ( len ( GoB g)) by MATRIX_0:def 10;

        then 1 <= ( len ( GoB g)) by NAT_1: 14;

        then

        consider i, j such that

         A63: i in ( dom g) and

         A64: [( len ( GoB g)), j] in ( Indices ( GoB g)) and

         A65: (g /. i) = (( GoB g) * (( len ( GoB g)),j)) by Th7;

        j in NAT by ORDINAL1:def 12;

        then j in Y by A63, A64, A65;

        then

        reconsider Y as non empty finite Subset of NAT by A61, A62;

        reconsider i1 = ( max Y) as Nat by TARSKI: 1;

        set s1 = ((( GoB g) * (( len ( GoB g)),( width ( GoB g)))) `2 );

        i1 in Y by XXREAL_2:def 8;

        then

        consider j be Element of NAT such that

         A66: j = i1 and

         A67: [( len ( GoB g)), j] in ( Indices ( GoB g)) and

         A68: ex i st i in ( dom g) & (g /. i) = (( GoB g) * (( len ( GoB g)),j));

        

         A69: i1 <= ( width ( GoB g)) by A66, A67, MATRIX_0: 32;

        

         A70: 1 <= ( len ( GoB g)) by A67, MATRIX_0: 32;

        1 <= i1 by A66, A67, MATRIX_0: 32;

        then

         A71: ((( GoB g) * (( len ( GoB g)),i1)) `1 ) = ((( GoB g) * (( len ( GoB g)),1)) `1 ) by A70, A69, GOBOARD5: 2;

        then

         A72: ((( GoB g) * (( len ( GoB g)),i1)) `1 ) = ( E-bound ( L~ g)) by Th39;

        consider i such that

         A73: i in ( dom g) and

         A74: (g /. i) = (( GoB g) * (( len ( GoB g)),j)) by A68;

        

         A75: i <= ( len g) by A73, FINSEQ_3: 25;

        

         A76: 1 <= i by A73, FINSEQ_3: 25;

         A77:

        now

          per cases by A75, XXREAL_0: 1;

            case i < ( len g);

            then (i + 1) <= ( len g) by NAT_1: 13;

            then (g /. i) in ( LSeg (g,i)) by A76, TOPREAL1: 21;

            hence (( GoB g) * (( len ( GoB g)),i1)) in ( L~ g) by A66, A74, SPPOL_2: 17;

          end;

            case i = ( len g);

            then (g /. i) in ( LSeg (g,(i -' 1))) by Lm9, Th1;

            hence (( GoB g) * (( len ( GoB g)),i1)) in ( L~ g) by A66, A74, SPPOL_2: 17;

          end;

        end;

        ((( GoB g) * (( len ( GoB g)),i1)) `1 ) = ( E-bound ( L~ g)) by A71, Th39;

        then

         A78: ((( GoB g) * (( len ( GoB g)),i1)) `2 ) in { (q `2 ) : (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g) } by A77;

        for r be Real st r in B holds r <= ((( GoB g) * (( len ( GoB g)),i1)) `2 )

        proof

          let r be Real;

          assume r in B;

          then ex q st r = (q `2 ) & (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g);

          hence thesis by Lm4;

        end;

        then

         A79: ( upper_bound B) <= ((( GoB g) * (( len ( GoB g)),i1)) `2 ) by A78, SEQ_4: 45;

        s1 is UpperBound of B

        proof

          let r be ExtReal;

          assume r in B;

          then

           A80: ex q st r = (q `2 ) & (q `1 ) = ( E-bound ( L~ g)) & q in ( L~ g);

          1 <= ( len ( GoB g)) by GOBOARD7: 32;

          hence thesis by A80, Th34;

        end;

        then B is bounded_above;

        then ( upper_bound B) >= ((( GoB g) * (( len ( GoB g)),i1)) `2 ) by A78, SEQ_4:def 1;

        

        then ((( GoB g) * (( len ( GoB g)),i1)) `2 ) = ( upper_bound B) by A79, XXREAL_0: 1

        .= ( upper_bound ( proj2 | ( E-most ( L~ g)))) by Th14;

        hence thesis by A66, A67, A72, EUCLID: 53;

      end;

      uniqueness by GOBOARD1: 5;

      :: JORDAN5D:def5

      func i_w_s g -> Nat means

      : Def5: [it , 1] in ( Indices ( GoB g)) & (( GoB g) * (it ,1)) = ( S-min ( L~ g));

      existence

      proof

        { (q `1 ) : (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g) } c= REAL

        proof

          let X be object;

          assume X in { (q `1 ) : (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g) };

          then ex q st X = (q `1 ) & (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g);

          hence thesis by XREAL_0:def 1;

        end;

        then

        reconsider B = { (q `1 ) : (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g) } as Subset of REAL ;

        set s1 = ((( GoB g) * (1,1)) `1 );

        defpred P[ Nat] means [$1, 1] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * ($1,1));

        set Y = { j where j be Element of NAT : P[j] };

        

         A81: Y c= ( dom ( GoB g))

        proof

          let y be object;

          assume y in Y;

          then ex j be Element of NAT st y = j & [j, 1] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * (j,1));

          then [y, 1] in [:( dom ( GoB g)), ( Seg ( width ( GoB g))):] by MATRIX_0:def 4;

          hence thesis by ZFMISC_1: 87;

        end;

        

         A82: Y is Subset of NAT from DOMAIN_1:sch 7;

        

         A83: 1 <= ( width ( GoB g)) by GOBOARD7: 33;

        then

        consider i, j such that

         A84: i in ( dom g) and

         A85: [j, 1] in ( Indices ( GoB g)) and

         A86: (g /. i) = (( GoB g) * (j,1)) by Th8;

        j in NAT by ORDINAL1:def 12;

        then j in Y by A84, A85, A86;

        then

        reconsider Y as non empty finite Subset of NAT by A81, A82;

        set i1 = ( min Y);

        i1 in Y by XXREAL_2:def 7;

        then

        consider j be Element of NAT such that

         A87: j = i1 and

         A88: [j, 1] in ( Indices ( GoB g)) and

         A89: ex i st i in ( dom g) & (g /. i) = (( GoB g) * (j,1));

        

         A90: i1 <= ( len ( GoB g)) by A87, A88, MATRIX_0: 32;

        

         A91: 1 <= ( width ( GoB g)) by A88, MATRIX_0: 32;

        1 <= i1 by A87, A88, MATRIX_0: 32;

        then

         A92: ((( GoB g) * (i1,1)) `2 ) = ((( GoB g) * (1,1)) `2 ) by A90, A91, GOBOARD5: 1;

        then

         A93: ((( GoB g) * (i1,1)) `2 ) = ( S-bound ( L~ g)) by Th38;

        consider i such that

         A94: i in ( dom g) and

         A95: (g /. i) = (( GoB g) * (j,1)) by A89;

        

         A96: i <= ( len g) by A94, FINSEQ_3: 25;

        

         A97: 1 <= i by A94, FINSEQ_3: 25;

         A98:

        now

          per cases by A96, XXREAL_0: 1;

            case i < ( len g);

            then (i + 1) <= ( len g) by NAT_1: 13;

            then (g /. i) in ( LSeg (g,i)) by A97, TOPREAL1: 21;

            hence (( GoB g) * (i1,1)) in ( L~ g) by A87, A95, SPPOL_2: 17;

          end;

            case i = ( len g);

            then (g /. i) in ( LSeg (g,(i -' 1))) by Lm9, Th1;

            hence (( GoB g) * (i1,1)) in ( L~ g) by A87, A95, SPPOL_2: 17;

          end;

        end;

        ((( GoB g) * (i1,1)) `2 ) = ( S-bound ( L~ g)) by A92, Th38;

        then

         A99: ((( GoB g) * (i1,1)) `1 ) in { (q `1 ) : (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g) } by A98;

        for r be Real st r in B holds r >= ((( GoB g) * (i1,1)) `1 )

        proof

          let r be Real;

          assume r in B;

          then ex q st r = (q `1 ) & (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g);

          hence thesis by Lm5;

        end;

        then

         A100: ( lower_bound B) >= ((( GoB g) * (i1,1)) `1 ) by A99, SEQ_4: 43;

        s1 is LowerBound of B

        proof

          let r be ExtReal;

          assume r in B;

          then ex q st r = (q `1 ) & (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g);

          hence thesis by A83, Th31;

        end;

        then B is bounded_below;

        then ( lower_bound B) <= ((( GoB g) * (i1,1)) `1 ) by A99, SEQ_4:def 2;

        

        then ((( GoB g) * (i1,1)) `1 ) = ( lower_bound B) by A100, XXREAL_0: 1

        .= ( lower_bound ( proj1 | ( S-most ( L~ g)))) by Th16;

        hence thesis by A87, A88, A93, EUCLID: 53;

      end;

      uniqueness by GOBOARD1: 5;

      :: JORDAN5D:def6

      func i_e_s g -> Nat means

      : Def6: [it , 1] in ( Indices ( GoB g)) & (( GoB g) * (it ,1)) = ( S-max ( L~ g));

      existence

      proof

        { (q `1 ) : (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g) } c= REAL

        proof

          let X be object;

          assume X in { (q `1 ) : (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g) };

          then ex q st X = (q `1 ) & (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g);

          hence thesis by XREAL_0:def 1;

        end;

        then

        reconsider B = { (q `1 ) : (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g) } as Subset of REAL ;

        defpred P[ Nat] means [$1, 1] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * ($1,1));

        set Y = { j where j be Element of NAT : P[j] };

        

         A101: Y c= ( dom ( GoB g))

        proof

          let y be object;

          assume y in Y;

          then ex j be Element of NAT st y = j & [j, 1] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * (j,1));

          then [y, 1] in [:( dom ( GoB g)), ( Seg ( width ( GoB g))):] by MATRIX_0:def 4;

          hence thesis by ZFMISC_1: 87;

        end;

        

         A102: Y is Subset of NAT from DOMAIN_1:sch 7;

        1 <= ( width ( GoB g)) by GOBOARD7: 33;

        then

        consider i, j such that

         A103: i in ( dom g) and

         A104: [j, 1] in ( Indices ( GoB g)) and

         A105: (g /. i) = (( GoB g) * (j,1)) by Th8;

        j in NAT by ORDINAL1:def 12;

        then j in Y by A103, A104, A105;

        then

        reconsider Y as non empty finite Subset of NAT by A101, A102;

        reconsider i1 = ( max Y) as Nat by TARSKI: 1;

        set s1 = ((( GoB g) * (( len ( GoB g)),1)) `1 );

        i1 in Y by XXREAL_2:def 8;

        then

        consider j be Element of NAT such that

         A106: j = i1 and

         A107: [j, 1] in ( Indices ( GoB g)) and

         A108: ex i st i in ( dom g) & (g /. i) = (( GoB g) * (j,1));

        

         A109: i1 <= ( len ( GoB g)) by A106, A107, MATRIX_0: 32;

        

         A110: 1 <= ( width ( GoB g)) by A107, MATRIX_0: 32;

        1 <= i1 by A106, A107, MATRIX_0: 32;

        then

         A111: ((( GoB g) * (i1,1)) `2 ) = ((( GoB g) * (1,1)) `2 ) by A109, A110, GOBOARD5: 1;

        then

         A112: ((( GoB g) * (i1,1)) `2 ) = ( S-bound ( L~ g)) by Th38;

        consider i such that

         A113: i in ( dom g) and

         A114: (g /. i) = (( GoB g) * (j,1)) by A108;

        

         A115: i <= ( len g) by A113, FINSEQ_3: 25;

        

         A116: 1 <= i by A113, FINSEQ_3: 25;

         A117:

        now

          per cases by A115, XXREAL_0: 1;

            case i < ( len g);

            then (i + 1) <= ( len g) by NAT_1: 13;

            then (g /. i) in ( LSeg (g,i)) by A116, TOPREAL1: 21;

            hence (( GoB g) * (i1,1)) in ( L~ g) by A106, A114, SPPOL_2: 17;

          end;

            case i = ( len g);

            then (g /. i) in ( LSeg (g,(i -' 1))) by Lm9, Th1;

            hence (( GoB g) * (i1,1)) in ( L~ g) by A106, A114, SPPOL_2: 17;

          end;

        end;

        ((( GoB g) * (i1,1)) `2 ) = ( S-bound ( L~ g)) by A111, Th38;

        then

         A118: ((( GoB g) * (i1,1)) `1 ) in { (q `1 ) : (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g) } by A117;

        for r be Real st r in B holds r <= ((( GoB g) * (i1,1)) `1 )

        proof

          let r be Real;

          assume r in B;

          then ex q st r = (q `1 ) & (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g);

          hence thesis by Lm7;

        end;

        then

         A119: ( upper_bound B) <= ((( GoB g) * (i1,1)) `1 ) by A118, SEQ_4: 45;

        s1 is UpperBound of B

        proof

          let r be ExtReal;

          assume r in B;

          then

           A120: ex q st r = (q `1 ) & (q `2 ) = ( S-bound ( L~ g)) & q in ( L~ g);

          1 <= ( width ( GoB g)) by GOBOARD7: 33;

          hence thesis by A120, Th32;

        end;

        then B is bounded_above;

        then ( upper_bound B) >= ((( GoB g) * (i1,1)) `1 ) by A118, SEQ_4:def 1;

        

        then ((( GoB g) * (i1,1)) `1 ) = ( upper_bound B) by A119, XXREAL_0: 1

        .= ( upper_bound ( proj1 | ( S-most ( L~ g)))) by Th16;

        hence thesis by A106, A107, A112, EUCLID: 53;

      end;

      uniqueness by GOBOARD1: 5;

      :: JORDAN5D:def7

      func i_w_n g -> Nat means

      : Def7: [it , ( width ( GoB g))] in ( Indices ( GoB g)) & (( GoB g) * (it ,( width ( GoB g)))) = ( N-min ( L~ g));

      existence

      proof

        { (q `1 ) : (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g) } c= REAL

        proof

          let X be object;

          assume X in { (q `1 ) : (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g) };

          then ex q st X = (q `1 ) & (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g);

          hence thesis by XREAL_0:def 1;

        end;

        then

        reconsider B = { (q `1 ) : (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g) } as Subset of REAL ;

        defpred P[ Nat] means [$1, ( width ( GoB g))] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * ($1,( width ( GoB g))));

        set Y = { j where j be Element of NAT : P[j] };

        

         A121: Y c= ( dom ( GoB g))

        proof

          let y be object;

          assume y in Y;

          then ex j be Element of NAT st y = j & [j, ( width ( GoB g))] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * (j,( width ( GoB g))));

          then [y, ( width ( GoB g))] in [:( dom ( GoB g)), ( Seg ( width ( GoB g))):] by MATRIX_0:def 4;

          hence thesis by ZFMISC_1: 87;

        end;

        

         A122: Y is Subset of NAT from DOMAIN_1:sch 7;

        1 <= ( width ( GoB g)) by GOBOARD7: 33;

        then

        consider i, j such that

         A123: i in ( dom g) and

         A124: [j, ( width ( GoB g))] in ( Indices ( GoB g)) and

         A125: (g /. i) = (( GoB g) * (j,( width ( GoB g)))) by Th8;

        j in NAT by ORDINAL1:def 12;

        then j in Y by A123, A124, A125;

        then

        reconsider Y as non empty finite Subset of NAT by A121, A122;

        set i1 = ( min Y);

        set s1 = ((( GoB g) * (1,( width ( GoB g)))) `1 );

        i1 in Y by XXREAL_2:def 7;

        then

        consider j be Element of NAT such that

         A126: j = i1 and

         A127: [j, ( width ( GoB g))] in ( Indices ( GoB g)) and

         A128: ex i be Nat st i in ( dom g) & (g /. i) = (( GoB g) * (j,( width ( GoB g))));

        

         A129: i1 <= ( len ( GoB g)) by A126, A127, MATRIX_0: 32;

        

         A130: 1 <= ( width ( GoB g)) by A127, MATRIX_0: 32;

        1 <= i1 by A126, A127, MATRIX_0: 32;

        then

         A131: ((( GoB g) * (i1,( width ( GoB g)))) `2 ) = ((( GoB g) * (1,( width ( GoB g)))) `2 ) by A129, A130, GOBOARD5: 1;

        then

         A132: ((( GoB g) * (i1,( width ( GoB g)))) `2 ) = ( N-bound ( L~ g)) by Th40;

        consider i such that

         A133: i in ( dom g) and

         A134: (g /. i) = (( GoB g) * (j,( width ( GoB g)))) by A128;

        

         A135: i <= ( len g) by A133, FINSEQ_3: 25;

        

         A136: 1 <= i by A133, FINSEQ_3: 25;

         A137:

        now

          per cases by A135, XXREAL_0: 1;

            case i < ( len g);

            then (i + 1) <= ( len g) by NAT_1: 13;

            then (g /. i) in ( LSeg (g,i)) by A136, TOPREAL1: 21;

            hence (( GoB g) * (i1,( width ( GoB g)))) in ( L~ g) by A126, A134, SPPOL_2: 17;

          end;

            case i = ( len g);

            then (g /. i) in ( LSeg (g,(i -' 1))) by Lm9, Th1;

            hence (( GoB g) * (i1,( width ( GoB g)))) in ( L~ g) by A126, A134, SPPOL_2: 17;

          end;

        end;

        ((( GoB g) * (i1,( width ( GoB g)))) `2 ) = ( N-bound ( L~ g)) by A131, Th40;

        then

         A138: ((( GoB g) * (i1,( width ( GoB g)))) `1 ) in { (q `1 ) : (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g) } by A137;

        for r be Real st r in B holds r >= ((( GoB g) * (i1,( width ( GoB g)))) `1 )

        proof

          let r be Real;

          assume r in B;

          then ex q st r = (q `1 ) & (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g);

          hence thesis by Lm6;

        end;

        then

         A139: ( lower_bound B) >= ((( GoB g) * (i1,( width ( GoB g)))) `1 ) by A138, SEQ_4: 43;

        s1 is LowerBound of B

        proof

          let r be ExtReal;

          assume r in B;

          then

           A140: ex q1 be Point of ( TOP-REAL 2) st r = (q1 `1 ) & (q1 `2 ) = ( N-bound ( L~ g)) & q1 in ( L~ g);

          1 <= ( width ( GoB g)) by GOBOARD7: 33;

          hence thesis by A140, Th31;

        end;

        then B is bounded_below;

        then ( lower_bound B) <= ((( GoB g) * (i1,( width ( GoB g)))) `1 ) by A138, SEQ_4:def 2;

        

        then ((( GoB g) * (i1,( width ( GoB g)))) `1 ) = ( lower_bound B) by A139, XXREAL_0: 1

        .= ( lower_bound ( proj1 | ( N-most ( L~ g)))) by Th15;

        hence thesis by A126, A127, A132, EUCLID: 53;

      end;

      uniqueness by GOBOARD1: 5;

      :: JORDAN5D:def8

      func i_e_n g -> Nat means

      : Def8: [it , ( width ( GoB g))] in ( Indices ( GoB g)) & (( GoB g) * (it ,( width ( GoB g)))) = ( N-max ( L~ g));

      existence

      proof

        { (q `1 ) : (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g) } c= REAL

        proof

          let X be object;

          assume X in { (q `1 ) : (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g) };

          then ex q st X = (q `1 ) & (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g);

          hence thesis by XREAL_0:def 1;

        end;

        then

        reconsider B = { (q `1 ) : (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g) } as Subset of REAL ;

        defpred P[ Nat] means [$1, ( width ( GoB g))] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * ($1,( width ( GoB g))));

        set Y = { j where j be Element of NAT : P[j] };

        

         A141: Y c= ( dom ( GoB g))

        proof

          let y be object;

          assume y in Y;

          then ex j be Element of NAT st y = j & [j, ( width ( GoB g))] in ( Indices ( GoB g)) & ex i st i in ( dom g) & (g /. i) = (( GoB g) * (j,( width ( GoB g))));

          then [y, ( width ( GoB g))] in [:( dom ( GoB g)), ( Seg ( width ( GoB g))):] by MATRIX_0:def 4;

          hence thesis by ZFMISC_1: 87;

        end;

        

         A142: Y is Subset of NAT from DOMAIN_1:sch 7;

        1 <= ( width ( GoB g)) by GOBOARD7: 33;

        then

        consider i, j such that

         A143: i in ( dom g) and

         A144: [j, ( width ( GoB g))] in ( Indices ( GoB g)) and

         A145: (g /. i) = (( GoB g) * (j,( width ( GoB g)))) by Th8;

        j in NAT by ORDINAL1:def 12;

        then j in Y by A143, A144, A145;

        then

        reconsider Y as non empty finite Subset of NAT by A141, A142;

        reconsider i1 = ( max Y) as Nat by TARSKI: 1;

        set s1 = ((( GoB g) * (( len ( GoB g)),( width ( GoB g)))) `1 );

        i1 in Y by XXREAL_2:def 8;

        then

        consider j be Element of NAT such that

         A146: j = i1 and

         A147: [j, ( width ( GoB g))] in ( Indices ( GoB g)) and

         A148: ex i be Nat st i in ( dom g) & (g /. i) = (( GoB g) * (j,( width ( GoB g))));

        

         A149: i1 <= ( len ( GoB g)) by A146, A147, MATRIX_0: 32;

        

         A150: 1 <= ( width ( GoB g)) by A147, MATRIX_0: 32;

        1 <= i1 by A146, A147, MATRIX_0: 32;

        then

         A151: ((( GoB g) * (i1,( width ( GoB g)))) `2 ) = ((( GoB g) * (1,( width ( GoB g)))) `2 ) by A149, A150, GOBOARD5: 1;

        then

         A152: ((( GoB g) * (i1,( width ( GoB g)))) `2 ) = ( N-bound ( L~ g)) by Th40;

        consider i such that

         A153: i in ( dom g) and

         A154: (g /. i) = (( GoB g) * (j,( width ( GoB g)))) by A148;

        

         A155: i <= ( len g) by A153, FINSEQ_3: 25;

        

         A156: 1 <= i by A153, FINSEQ_3: 25;

         A157:

        now

          per cases by A155, XXREAL_0: 1;

            case i < ( len g);

            then (i + 1) <= ( len g) by NAT_1: 13;

            then (g /. i) in ( LSeg (g,i)) by A156, TOPREAL1: 21;

            hence (( GoB g) * (i1,( width ( GoB g)))) in ( L~ g) by A146, A154, SPPOL_2: 17;

          end;

            case i = ( len g);

            then (g /. i) in ( LSeg (g,(i -' 1))) by Lm9, Th1;

            hence (( GoB g) * (i1,( width ( GoB g)))) in ( L~ g) by A146, A154, SPPOL_2: 17;

          end;

        end;

        ((( GoB g) * (i1,( width ( GoB g)))) `2 ) = ( N-bound ( L~ g)) by A151, Th40;

        then

         A158: ((( GoB g) * (i1,( width ( GoB g)))) `1 ) in { (q `1 ) : (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g) } by A157;

        for r be Real st r in B holds r <= ((( GoB g) * (i1,( width ( GoB g)))) `1 )

        proof

          let r be Real;

          assume r in B;

          then ex q st r = (q `1 ) & (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g);

          hence thesis by Lm8;

        end;

        then

         A159: ( upper_bound B) <= ((( GoB g) * (i1,( width ( GoB g)))) `1 ) by A158, SEQ_4: 45;

        s1 is UpperBound of B

        proof

          let r be ExtReal;

          assume r in B;

          then

           A160: ex q st r = (q `1 ) & (q `2 ) = ( N-bound ( L~ g)) & q in ( L~ g);

          1 <= ( width ( GoB g)) by GOBOARD7: 33;

          hence thesis by A160, Th32;

        end;

        then B is bounded_above;

        then ( upper_bound B) >= ((( GoB g) * (i1,( width ( GoB g)))) `1 ) by A158, SEQ_4:def 1;

        

        then ((( GoB g) * (i1,( width ( GoB g)))) `1 ) = ( upper_bound B) by A159, XXREAL_0: 1

        .= ( upper_bound ( proj1 | ( N-most ( L~ g)))) by Th15;

        hence thesis by A146, A147, A152, EUCLID: 53;

      end;

      uniqueness by GOBOARD1: 5;

    end

    theorem :: JORDAN5D:45

    1 <= ( i_w_n h) & ( i_w_n h) <= ( len ( GoB h)) & 1 <= ( i_e_n h) & ( i_e_n h) <= ( len ( GoB h)) & 1 <= ( i_w_s h) & ( i_w_s h) <= ( len ( GoB h)) & 1 <= ( i_e_s h) & ( i_e_s h) <= ( len ( GoB h))

    proof

      

       A1: [( i_e_n h), ( width ( GoB h))] in ( Indices ( GoB h)) by Def8;

      

       A2: [( i_w_s h), 1] in ( Indices ( GoB h)) by Def5;

      

       A3: [( i_e_s h), 1] in ( Indices ( GoB h)) by Def6;

       [( i_w_n h), ( width ( GoB h))] in ( Indices ( GoB h)) by Def7;

      hence thesis by A1, A2, A3, MATRIX_0: 32;

    end;

    theorem :: JORDAN5D:46

    1 <= ( i_n_e h) & ( i_n_e h) <= ( width ( GoB h)) & 1 <= ( i_s_e h) & ( i_s_e h) <= ( width ( GoB h)) & 1 <= ( i_n_w h) & ( i_n_w h) <= ( width ( GoB h)) & 1 <= ( i_s_w h) & ( i_s_w h) <= ( width ( GoB h))

    proof

      

       A1: [( len ( GoB h)), ( i_s_e h)] in ( Indices ( GoB h)) by Def3;

      

       A2: [1, ( i_n_w h)] in ( Indices ( GoB h)) by Def2;

      

       A3: [1, ( i_s_w h)] in ( Indices ( GoB h)) by Def1;

       [( len ( GoB h)), ( i_n_e h)] in ( Indices ( GoB h)) by Def4;

      hence thesis by A1, A2, A3, MATRIX_0: 32;

    end;

    

     Lm10: for i1,i2 be Nat st 1 <= i1 & (i1 + 1) <= ( len h) & 1 <= i2 & (i2 + 1) <= ( len h) & (h . i1) = (h . i2) holds i1 = i2

    proof

      let i1,i2 be Nat;

      assume that

       A1: 1 <= i1 and

       A2: (i1 + 1) <= ( len h);

      

       A3: i1 < ( len h) by A2, NAT_1: 13;

      assume that

       A4: 1 <= i2 and

       A5: (i2 + 1) <= ( len h) and

       A6: (h . i1) = (h . i2);

      

       A7: i2 < ( len h) by A5, NAT_1: 13;

      then

       A8: i2 in ( dom h) by A4, FINSEQ_3: 25;

      assume

       A9: i1 <> i2;

       A10:

      now

        per cases by A9, XXREAL_0: 1;

          suppose i1 < i2;

          hence (h /. i1) <> (h /. i2) by A1, A7, GOBOARD7: 36;

        end;

          suppose i2 < i1;

          hence (h /. i1) <> (h /. i2) by A4, A3, GOBOARD7: 36;

        end;

      end;

      i1 in ( dom h) by A1, A3, FINSEQ_3: 25;

      

      then (h /. i1) = (h . i2) by A6, PARTFUN1:def 6

      .= (h /. i2) by A8, PARTFUN1:def 6;

      hence thesis by A10;

    end;

    definition

      let g be non constant standard special_circular_sequence;

      :: JORDAN5D:def9

      func n_s_w g -> Nat means

      : Def9: 1 <= it & (it + 1) <= ( len g) & (g . it ) = ( W-min ( L~ g));

      existence

      proof

        ( W-min ( L~ g)) in ( rng g) by SPRECT_2: 43;

        hence thesis by Th3;

      end;

      uniqueness by Lm10;

      :: JORDAN5D:def10

      func n_n_w g -> Nat means

      : Def10: 1 <= it & (it + 1) <= ( len g) & (g . it ) = ( W-max ( L~ g));

      existence

      proof

        ( W-max ( L~ g)) in ( rng g) by SPRECT_2: 44;

        hence thesis by Th3;

      end;

      uniqueness by Lm10;

      :: JORDAN5D:def11

      func n_s_e g -> Nat means

      : Def11: 1 <= it & (it + 1) <= ( len g) & (g . it ) = ( E-min ( L~ g));

      existence

      proof

        ( E-min ( L~ g)) in ( rng g) by SPRECT_2: 45;

        hence thesis by Th3;

      end;

      uniqueness by Lm10;

      :: JORDAN5D:def12

      func n_n_e g -> Nat means

      : Def12: 1 <= it & (it + 1) <= ( len g) & (g . it ) = ( E-max ( L~ g));

      existence

      proof

        ( E-max ( L~ g)) in ( rng g) by SPRECT_2: 46;

        hence thesis by Th3;

      end;

      uniqueness by Lm10;

      :: JORDAN5D:def13

      func n_w_s g -> Nat means

      : Def13: 1 <= it & (it + 1) <= ( len g) & (g . it ) = ( S-min ( L~ g));

      existence

      proof

        ( S-min ( L~ g)) in ( rng g) by SPRECT_2: 41;

        hence thesis by Th3;

      end;

      uniqueness by Lm10;

      :: JORDAN5D:def14

      func n_e_s g -> Nat means

      : Def14: 1 <= it & (it + 1) <= ( len g) & (g . it ) = ( S-max ( L~ g));

      existence

      proof

        ( S-max ( L~ g)) in ( rng g) by SPRECT_2: 42;

        hence thesis by Th3;

      end;

      uniqueness by Lm10;

      :: JORDAN5D:def15

      func n_w_n g -> Nat means

      : Def15: 1 <= it & (it + 1) <= ( len g) & (g . it ) = ( N-min ( L~ g));

      existence

      proof

        ( N-min ( L~ g)) in ( rng g) by SPRECT_2: 39;

        hence thesis by Th3;

      end;

      uniqueness by Lm10;

      :: JORDAN5D:def16

      func n_e_n g -> Nat means

      : Def16: 1 <= it & (it + 1) <= ( len g) & (g . it ) = ( N-max ( L~ g));

      existence

      proof

        ( N-max ( L~ g)) in ( rng g) by SPRECT_2: 40;

        hence thesis by Th3;

      end;

      uniqueness by Lm10;

    end

    theorem :: JORDAN5D:47

    ( n_w_n h) <> ( n_w_s h)

    proof

      set i1 = ( n_w_n h), i2 = ( n_w_s h);

      

       A1: i1 <= (i1 + 1) by NAT_1: 11;

      

       A2: 1 <= i1 by Def15;

      (i1 + 1) <= ( len h) by Def15;

      then i1 <= ( len h) by A1, XXREAL_0: 2;

      then i1 in ( dom h) by A2, FINSEQ_3: 25;

      then

       A3: (h . i1) = (h /. i1) by PARTFUN1:def 6;

      

       A4: i2 <= (i2 + 1) by NAT_1: 11;

      

       A5: (h . i2) = ( S-min ( L~ h)) by Def13;

      

       A6: 1 <= i2 by Def13;

      (i2 + 1) <= ( len h) by Def13;

      then i2 <= ( len h) by A4, XXREAL_0: 2;

      then i2 in ( dom h) by A6, FINSEQ_3: 25;

      then

       A7: (h . i2) = (h /. i2) by PARTFUN1:def 6;

      

       A8: (h . i1) = ( N-min ( L~ h)) by Def15;

      thus i1 <> i2

      proof

        assume i1 = i2;

        

        then

         A9: ( N-bound ( L~ h)) = ((h /. i2) `2 ) by A8, A3, EUCLID: 52

        .= ( S-bound ( L~ h)) by A5, A7, EUCLID: 52;

        

         A10: 1 <= ( len h) by GOBOARD7: 34, XXREAL_0: 2;

        then

         A11: ((h /. 1) `2 ) >= ( S-bound ( L~ h)) by Th11;

        consider ii be Nat such that

         A12: ii in ( dom h) and

         A13: ((h /. ii) `2 ) <> ((h /. 1) `2 ) by GOBOARD7: 31;

        

         A14: ii <= ( len h) by A12, FINSEQ_3: 25;

        

         A15: 1 <= ii by A12, FINSEQ_3: 25;

        then

         A16: ((h /. ii) `2 ) <= ( N-bound ( L~ h)) by A14, Th11;

        

         A17: ((h /. ii) `2 ) >= ( S-bound ( L~ h)) by A15, A14, Th11;

        ((h /. 1) `2 ) <= ( N-bound ( L~ h)) by A10, Th11;

        then ((h /. 1) `2 ) = ( N-bound ( L~ h)) by A9, A11, XXREAL_0: 1;

        hence thesis by A9, A13, A16, A17, XXREAL_0: 1;

      end;

    end;

    theorem :: JORDAN5D:48

    ( n_s_w h) <> ( n_s_e h)

    proof

      set i1 = ( n_s_w h), i2 = ( n_s_e h);

      

       A1: i1 <= (i1 + 1) by NAT_1: 11;

      

       A2: 1 <= i1 by Def9;

      (i1 + 1) <= ( len h) by Def9;

      then i1 <= ( len h) by A1, XXREAL_0: 2;

      then i1 in ( dom h) by A2, FINSEQ_3: 25;

      then

       A3: (h . i1) = (h /. i1) by PARTFUN1:def 6;

      

       A4: i2 <= (i2 + 1) by NAT_1: 11;

      

       A5: (h . i2) = ( E-min ( L~ h)) by Def11;

      

       A6: 1 <= i2 by Def11;

      (i2 + 1) <= ( len h) by Def11;

      then i2 <= ( len h) by A4, XXREAL_0: 2;

      then i2 in ( dom h) by A6, FINSEQ_3: 25;

      then

       A7: (h . i2) = (h /. i2) by PARTFUN1:def 6;

      

       A8: (h . i1) = ( W-min ( L~ h)) by Def9;

      thus i1 <> i2

      proof

        assume i1 = i2;

        

        then

         A9: ( W-bound ( L~ h)) = ((h /. i2) `1 ) by A8, A3, EUCLID: 52

        .= ( E-bound ( L~ h)) by A5, A7, EUCLID: 52;

        

         A10: 1 <= ( len h) by GOBOARD7: 34, XXREAL_0: 2;

        then

         A11: ((h /. 1) `1 ) >= ( W-bound ( L~ h)) by Th12;

        consider ii be Nat such that

         A12: ii in ( dom h) and

         A13: ((h /. ii) `1 ) <> ((h /. 1) `1 ) by GOBOARD7: 30;

        

         A14: ii <= ( len h) by A12, FINSEQ_3: 25;

        

         A15: 1 <= ii by A12, FINSEQ_3: 25;

        then

         A16: ((h /. ii) `1 ) <= ( E-bound ( L~ h)) by A14, Th12;

        

         A17: ((h /. ii) `1 ) >= ( W-bound ( L~ h)) by A15, A14, Th12;

        ((h /. 1) `1 ) <= ( E-bound ( L~ h)) by A10, Th12;

        then ((h /. 1) `1 ) = ( W-bound ( L~ h)) by A9, A11, XXREAL_0: 1;

        hence thesis by A9, A13, A16, A17, XXREAL_0: 1;

      end;

    end;

    theorem :: JORDAN5D:49

    ( n_e_n h) <> ( n_e_s h)

    proof

      set i1 = ( n_e_n h), i2 = ( n_e_s h);

      

       A1: i1 <= (i1 + 1) by NAT_1: 11;

      

       A2: 1 <= i1 by Def16;

      (i1 + 1) <= ( len h) by Def16;

      then i1 <= ( len h) by A1, XXREAL_0: 2;

      then i1 in ( dom h) by A2, FINSEQ_3: 25;

      then

       A3: (h . i1) = (h /. i1) by PARTFUN1:def 6;

      

       A4: i2 <= (i2 + 1) by NAT_1: 11;

      

       A5: (h . i2) = ( S-max ( L~ h)) by Def14;

      

       A6: 1 <= i2 by Def14;

      (i2 + 1) <= ( len h) by Def14;

      then i2 <= ( len h) by A4, XXREAL_0: 2;

      then i2 in ( dom h) by A6, FINSEQ_3: 25;

      then

       A7: (h . i2) = (h /. i2) by PARTFUN1:def 6;

      

       A8: (h . i1) = ( N-max ( L~ h)) by Def16;

      thus i1 <> i2

      proof

        assume i1 = i2;

        

        then

         A9: ( N-bound ( L~ h)) = ((h /. i2) `2 ) by A8, A3, EUCLID: 52

        .= ( S-bound ( L~ h)) by A5, A7, EUCLID: 52;

        

         A10: 1 <= ( len h) by GOBOARD7: 34, XXREAL_0: 2;

        then

         A11: ((h /. 1) `2 ) >= ( S-bound ( L~ h)) by Th11;

        consider ii be Nat such that

         A12: ii in ( dom h) and

         A13: ((h /. ii) `2 ) <> ((h /. 1) `2 ) by GOBOARD7: 31;

        

         A14: ii <= ( len h) by A12, FINSEQ_3: 25;

        

         A15: 1 <= ii by A12, FINSEQ_3: 25;

        then

         A16: ((h /. ii) `2 ) <= ( N-bound ( L~ h)) by A14, Th11;

        

         A17: ((h /. ii) `2 ) >= ( S-bound ( L~ h)) by A15, A14, Th11;

        ((h /. 1) `2 ) <= ( N-bound ( L~ h)) by A10, Th11;

        then ((h /. 1) `2 ) = ( N-bound ( L~ h)) by A9, A11, XXREAL_0: 1;

        hence thesis by A9, A13, A16, A17, XXREAL_0: 1;

      end;

    end;

    theorem :: JORDAN5D:50

    ( n_n_w h) <> ( n_n_e h)

    proof

      set i1 = ( n_n_w h), i2 = ( n_n_e h);

      

       A1: i1 <= (i1 + 1) by NAT_1: 11;

      

       A2: 1 <= i1 by Def10;

      (i1 + 1) <= ( len h) by Def10;

      then i1 <= ( len h) by A1, XXREAL_0: 2;

      then i1 in ( dom h) by A2, FINSEQ_3: 25;

      then

       A3: (h . i1) = (h /. i1) by PARTFUN1:def 6;

      

       A4: i2 <= (i2 + 1) by NAT_1: 11;

      

       A5: (h . i2) = ( E-max ( L~ h)) by Def12;

      

       A6: 1 <= i2 by Def12;

      (i2 + 1) <= ( len h) by Def12;

      then i2 <= ( len h) by A4, XXREAL_0: 2;

      then i2 in ( dom h) by A6, FINSEQ_3: 25;

      then

       A7: (h . i2) = (h /. i2) by PARTFUN1:def 6;

      

       A8: (h . i1) = ( W-max ( L~ h)) by Def10;

      thus i1 <> i2

      proof

        assume i1 = i2;

        

        then

         A9: ( W-bound ( L~ h)) = ((h /. i2) `1 ) by A8, A3, EUCLID: 52

        .= ( E-bound ( L~ h)) by A5, A7, EUCLID: 52;

        

         A10: 1 <= ( len h) by GOBOARD7: 34, XXREAL_0: 2;

        then

         A11: ((h /. 1) `1 ) >= ( W-bound ( L~ h)) by Th12;

        consider ii be Nat such that

         A12: ii in ( dom h) and

         A13: ((h /. ii) `1 ) <> ((h /. 1) `1 ) by GOBOARD7: 30;

        

         A14: ii <= ( len h) by A12, FINSEQ_3: 25;

        

         A15: 1 <= ii by A12, FINSEQ_3: 25;

        then

         A16: ((h /. ii) `1 ) <= ( E-bound ( L~ h)) by A14, Th12;

        

         A17: ((h /. ii) `1 ) >= ( W-bound ( L~ h)) by A15, A14, Th12;

        ((h /. 1) `1 ) <= ( E-bound ( L~ h)) by A10, Th12;

        then ((h /. 1) `1 ) = ( W-bound ( L~ h)) by A9, A11, XXREAL_0: 1;

        hence thesis by A9, A13, A16, A17, XXREAL_0: 1;

      end;

    end;