sprect_2.miz



    begin

    reserve i,j,k,l,m,n for Nat,

D for non empty set,

f for FinSequence of D;

    theorem :: SPRECT_2:1

    

     Th1: i <= j & i in ( dom f) & j in ( dom f) & k in ( dom ( mid (f,i,j))) implies ((k + i) -' 1) in ( dom f)

    proof

      assume that

       A1: i <= j and

       A2: i in ( dom f) and

       A3: j in ( dom f);

      

       A4: j <= ( len f) by A3, FINSEQ_3: 25;

      

       A5: (1 + 0 ) <= i by A2, FINSEQ_3: 25;

      then (i - 1) >= 0 by XREAL_1: 19;

      then

       A6: (k + 0 ) <= (k + (i - 1)) by XREAL_1: 6;

      assume

       A7: k in ( dom ( mid (f,i,j)));

      then

       A8: k <= ( len ( mid (f,i,j))) by FINSEQ_3: 25;

      i <= ( len f) & 1 <= j by A2, A3, FINSEQ_3: 25;

      then ( len ( mid (f,i,j))) = ((j -' i) + 1) by A1, A5, A4, FINSEQ_6: 118;

      then k <= ((j - i) + 1) by A1, A8, XREAL_1: 233;

      then k <= ((j + 1) - i);

      then (k + i) <= (j + 1) by XREAL_1: 19;

      then (k + i) >= i & ((k + i) - 1) <= j by NAT_1: 11, XREAL_1: 20;

      then ((k + i) -' 1) <= j by A5, XREAL_1: 233, XXREAL_0: 2;

      then

       A9: ((k + i) -' 1) <= ( len f) by A4, XXREAL_0: 2;

      1 <= k by A7, FINSEQ_3: 25;

      then 1 <= ((k + i) - 1) by A6, XXREAL_0: 2;

      then 1 <= ((k + i) -' 1) by NAT_D: 39;

      hence thesis by A9, FINSEQ_3: 25;

    end;

    theorem :: SPRECT_2:2

    

     Th2: i > j & i in ( dom f) & j in ( dom f) & k in ( dom ( mid (f,i,j))) implies ((i -' k) + 1) in ( dom f)

    proof

      assume that

       A1: i > j and

       A2: i in ( dom f) and

       A3: j in ( dom f);

      

       A4: i <= ( len f) by A2, FINSEQ_3: 25;

      

       A5: (1 + 0 ) <= j by A3, FINSEQ_3: 25;

      then (1 - j) <= 0 by XREAL_1: 47;

      then

       A6: (i + (1 - j)) <= (i + 0 ) by XREAL_1: 6;

      assume

       A7: k in ( dom ( mid (f,i,j)));

      then

       A8: k <= ( len ( mid (f,i,j))) by FINSEQ_3: 25;

      k >= 1 by A7, FINSEQ_3: 25;

      then (1 - k) <= 0 by XREAL_1: 47;

      then (i + (1 - k)) <= (i + 0 ) by XREAL_1: 6;

      then

       A9: ((i - k) + 1) <= i;

      (1 + 0 ) <= i & j <= ( len f) by A2, A3, FINSEQ_3: 25;

      then ( len ( mid (f,i,j))) = ((i -' j) + 1) by A1, A4, A5, FINSEQ_6: 118;

      then k <= ((i - j) + 1) by A1, A8, XREAL_1: 233;

      then ((i -' k) + 1) <= i by A6, A9, XREAL_1: 233, XXREAL_0: 2;

      then

       A10: ((i -' k) + 1) <= ( len f) by A4, XXREAL_0: 2;

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

      hence thesis by A10, FINSEQ_3: 25;

    end;

    theorem :: SPRECT_2:3

    

     Th3: i <= j & i in ( dom f) & j in ( dom f) & k in ( dom ( mid (f,i,j))) implies (( mid (f,i,j)) /. k) = (f /. ((k + i) -' 1))

    proof

      assume that

       A1: i <= j and

       A2: i in ( dom f) and

       A3: j in ( dom f) and

       A4: k in ( dom ( mid (f,i,j)));

      

       A5: 1 <= i & i <= ( len f) by A2, FINSEQ_3: 25;

      

       A6: 1 <= k & k <= ( len ( mid (f,i,j))) by A4, FINSEQ_3: 25;

      

       A7: 1 <= j & j <= ( len f) by A3, FINSEQ_3: 25;

      

      thus (( mid (f,i,j)) /. k) = (( mid (f,i,j)) . k) by A4, PARTFUN1:def 6

      .= (f . ((k + i) -' 1)) by A1, A5, A7, A6, FINSEQ_6: 118

      .= (f /. ((k + i) -' 1)) by A1, A2, A3, A4, Th1, PARTFUN1:def 6;

    end;

    theorem :: SPRECT_2:4

    

     Th4: i > j & i in ( dom f) & j in ( dom f) & k in ( dom ( mid (f,i,j))) implies (( mid (f,i,j)) /. k) = (f /. ((i -' k) + 1))

    proof

      assume that

       A1: i > j and

       A2: i in ( dom f) and

       A3: j in ( dom f) and

       A4: k in ( dom ( mid (f,i,j)));

      

       A5: 1 <= i & i <= ( len f) by A2, FINSEQ_3: 25;

      

       A6: 1 <= k & k <= ( len ( mid (f,i,j))) by A4, FINSEQ_3: 25;

      

       A7: 1 <= j & j <= ( len f) by A3, FINSEQ_3: 25;

      

      thus (( mid (f,i,j)) /. k) = (( mid (f,i,j)) . k) by A4, PARTFUN1:def 6

      .= (f . ((i -' k) + 1)) by A1, A5, A7, A6, FINSEQ_6: 118

      .= (f /. ((i -' k) + 1)) by A1, A2, A3, A4, Th2, PARTFUN1:def 6;

    end;

    theorem :: SPRECT_2:5

    

     Th5: i in ( dom f) & j in ( dom f) implies ( len ( mid (f,i,j))) >= 1

    proof

      

       A1: i <= j or j < i;

      assume i in ( dom f);

      then

       A2: 1 <= i & i <= ( len f) by FINSEQ_3: 25;

      assume j in ( dom f);

      then 1 <= j & j <= ( len f) by FINSEQ_3: 25;

      then ( len ( mid (f,i,j))) = ((i -' j) + 1) or ( len ( mid (f,i,j))) = ((j -' i) + 1) by A2, A1, FINSEQ_6: 118;

      hence thesis by NAT_1: 11;

    end;

    theorem :: SPRECT_2:6

    

     Th6: i in ( dom f) & j in ( dom f) & ( len ( mid (f,i,j))) = 1 implies i = j

    proof

      assume

       A1: i in ( dom f);

      then

       A2: 1 <= i by FINSEQ_3: 25;

      

       A3: i <= ( len f) by A1, FINSEQ_3: 25;

      assume

       A4: j in ( dom f);

      then

       A5: 1 <= j by FINSEQ_3: 25;

      

       A6: j <= ( len f) by A4, FINSEQ_3: 25;

      assume

       A7: ( len ( mid (f,i,j))) = 1;

      per cases ;

        suppose

         A8: i <= j;

        then ( 0 + 1) = ((j -' i) + 1) by A2, A6, A7, JORDAN4: 8;

        then 0 = (j - i) by A8, XREAL_1: 233;

        hence thesis;

      end;

        suppose

         A9: i >= j;

        then ( 0 + 1) = ((i -' j) + 1) by A3, A5, A7, JORDAN4: 9;

        then 0 = (i - j) by A9, XREAL_1: 233;

        hence thesis;

      end;

    end;

    theorem :: SPRECT_2:7

    

     Th7: i in ( dom f) & j in ( dom f) implies ( mid (f,i,j)) is non empty

    proof

      assume i in ( dom f) & j in ( dom f);

      then ( len ( mid (f,i,j))) >= 1 by Th5;

      hence thesis by FINSEQ_3: 25, RELAT_1: 38;

    end;

    theorem :: SPRECT_2:8

    

     Th8: i in ( dom f) & j in ( dom f) implies (( mid (f,i,j)) /. 1) = (f /. i)

    proof

      assume

       A1: i in ( dom f);

      then

       A2: 1 <= i & i <= ( len f) by FINSEQ_3: 25;

      assume

       A3: j in ( dom f);

      then

       A4: 1 <= j & j <= ( len f) by FINSEQ_3: 25;

      ( mid (f,i,j)) is non empty by A1, A3, Th7;

      then 1 in ( dom ( mid (f,i,j))) by FINSEQ_5: 6;

      

      hence (( mid (f,i,j)) /. 1) = (( mid (f,i,j)) . 1) by PARTFUN1:def 6

      .= (f . i) by A2, A4, FINSEQ_6: 118

      .= (f /. i) by A1, PARTFUN1:def 6;

    end;

    theorem :: SPRECT_2:9

    

     Th9: i in ( dom f) & j in ( dom f) implies (( mid (f,i,j)) /. ( len ( mid (f,i,j)))) = (f /. j)

    proof

      assume

       A1: i in ( dom f);

      then

       A2: 1 <= i & i <= ( len f) by FINSEQ_3: 25;

      assume

       A3: j in ( dom f);

      then

       A4: 1 <= j & j <= ( len f) by FINSEQ_3: 25;

      ( mid (f,i,j)) is non empty by A1, A3, Th7;

      then ( len ( mid (f,i,j))) in ( dom ( mid (f,i,j))) by FINSEQ_5: 6;

      

      hence (( mid (f,i,j)) /. ( len ( mid (f,i,j)))) = (( mid (f,i,j)) . ( len ( mid (f,i,j)))) by PARTFUN1:def 6

      .= (f . j) by A2, A4, JORDAN4: 11

      .= (f /. j) by A3, PARTFUN1:def 6;

    end;

    begin

    reserve X for compact Subset of ( TOP-REAL 2);

    theorem :: SPRECT_2:10

    

     Th10: for p be Point of ( TOP-REAL 2) st p in X & (p `2 ) = ( N-bound X) holds p in ( N-most X)

    proof

      let p be Point of ( TOP-REAL 2) such that

       A1: p in X and

       A2: (p `2 ) = ( N-bound X);

      

       A3: (( NW-corner X) `2 ) = ( N-bound X) & (( NE-corner X) `2 ) = ( N-bound X) by EUCLID: 52;

      

       A4: (( NW-corner X) `1 ) = ( W-bound X) & (( NE-corner X) `1 ) = ( E-bound X) by EUCLID: 52;

      ( W-bound X) <= (p `1 ) & (p `1 ) <= ( E-bound X) by A1, PSCOMP_1: 24;

      then p in ( LSeg (( NW-corner X),( NE-corner X))) by A2, A3, A4, GOBOARD7: 8;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: SPRECT_2:11

    

     Th11: for p be Point of ( TOP-REAL 2) st p in X & (p `2 ) = ( S-bound X) holds p in ( S-most X)

    proof

      let p be Point of ( TOP-REAL 2) such that

       A1: p in X and

       A2: (p `2 ) = ( S-bound X);

      

       A3: (( SW-corner X) `2 ) = ( S-bound X) & (( SE-corner X) `2 ) = ( S-bound X) by EUCLID: 52;

      

       A4: (( SW-corner X) `1 ) = ( W-bound X) & (( SE-corner X) `1 ) = ( E-bound X) by EUCLID: 52;

      ( W-bound X) <= (p `1 ) & (p `1 ) <= ( E-bound X) by A1, PSCOMP_1: 24;

      then p in ( LSeg (( SW-corner X),( SE-corner X))) by A2, A3, A4, GOBOARD7: 8;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: SPRECT_2:12

    

     Th12: for p be Point of ( TOP-REAL 2) st p in X & (p `1 ) = ( W-bound X) holds p in ( W-most X)

    proof

      let p be Point of ( TOP-REAL 2) such that

       A1: p in X and

       A2: (p `1 ) = ( W-bound X);

      

       A3: (( SW-corner X) `1 ) = ( W-bound X) & (( NW-corner X) `1 ) = ( W-bound X) by EUCLID: 52;

      

       A4: (( SW-corner X) `2 ) = ( S-bound X) & (( NW-corner X) `2 ) = ( N-bound X) by EUCLID: 52;

      ( S-bound X) <= (p `2 ) & (p `2 ) <= ( N-bound X) by A1, PSCOMP_1: 24;

      then p in ( LSeg (( SW-corner X),( NW-corner X))) by A2, A3, A4, GOBOARD7: 7;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: SPRECT_2:13

    

     Th13: for p be Point of ( TOP-REAL 2) st p in X & (p `1 ) = ( E-bound X) holds p in ( E-most X)

    proof

      let p be Point of ( TOP-REAL 2) such that

       A1: p in X and

       A2: (p `1 ) = ( E-bound X);

      

       A3: (( SE-corner X) `1 ) = ( E-bound X) & (( NE-corner X) `1 ) = ( E-bound X) by EUCLID: 52;

      

       A4: (( SE-corner X) `2 ) = ( S-bound X) & (( NE-corner X) `2 ) = ( N-bound X) by EUCLID: 52;

      ( S-bound X) <= (p `2 ) & (p `2 ) <= ( N-bound X) by A1, PSCOMP_1: 24;

      then p in ( LSeg (( SE-corner X),( NE-corner X))) by A2, A3, A4, GOBOARD7: 7;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    begin

    theorem :: SPRECT_2:14

    

     Th14: for f be FinSequence of ( TOP-REAL 2) st 1 <= i & i <= j & j <= ( len f) holds ( L~ ( mid (f,i,j))) = ( union { ( LSeg (f,k)) : i <= k & k < j })

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume that

       A1: 1 <= i and

       A2: i <= j and

       A3: j <= ( len f);

      set A = { ( LSeg (( mid (f,i,j)),m)) : 1 <= m & (m + 1) <= ( len ( mid (f,i,j))) }, B = { ( LSeg (f,l)) : i <= l & l < j };

      per cases by A2, XXREAL_0: 1;

        suppose

         A4: i = j;

        

         A5: B = {}

        proof

          assume B <> {} ;

          then

          consider z be object such that

           A6: z in B by XBOOLE_0:def 1;

          ex l st z = ( LSeg (f,l)) & i <= l & l < j by A6;

          hence contradiction by A4;

        end;

        

         AA: i in ( dom f) by FINSEQ_3: 25, A1, A3, A4;

        

        then ( mid (f,i,j)) = <*(f . i)*> by A4, JORDAN4: 15

        .= <*(f /. i)*> by AA, PARTFUN1:def 6;

        hence thesis by A5, SPPOL_2: 12, ZFMISC_1: 2;

      end;

        suppose

         A7: i < j;

        A = B

        proof

          hereby

            let x be object;

            assume x in A;

            then

            consider m such that

             A8: x = ( LSeg (( mid (f,i,j)),m)) and

             A9: ( 0 + 1) <= m and

             A10: (m + 1) <= ( len ( mid (f,i,j)));

            i < (m + i) by A9, XREAL_1: 29;

            then

             A11: i <= ((m + i) -' 1) by NAT_D: 49;

            ( len ( mid (f,i,j))) = ((j -' i) + 1) by A1, A3, A7, JORDAN4: 8;

            then

             A12: m < ((j -' i) + 1) by A10, NAT_1: 13;

            then m <= (j -' i) by NAT_1: 13;

            then m <= (j - i) by A7, XREAL_1: 233;

            then (m + i) >= m & (m + i) <= j by NAT_1: 11, XREAL_1: 19;

            then (((m + i) -' 1) + 1) <= j by A9, XREAL_1: 235, XXREAL_0: 2;

            then

             A13: ((m + i) -' 1) < j by NAT_1: 13;

            x = ( LSeg (f,((m + i) -' 1))) by A1, A3, A7, A8, A9, A12, JORDAN4: 19;

            hence x in B by A13, A11;

          end;

          let x be object;

          assume x in B;

          then

          consider l such that

           A14: x = ( LSeg (f,l)) and

           A15: i <= l and

           A16: l < j;

          set m = ((l -' i) + 1);

          

           A17: (l - i) < (j - i) by A16, XREAL_1: 9;

          (l -' i) = (l - i) & (j -' i) = (j - i) by A15, A16, XREAL_1: 233, XXREAL_0: 2;

          then

           A18: m < ((j -' i) + 1) by A17, XREAL_1: 6;

          ( len ( mid (f,i,j))) = ((j -' i) + 1) by A1, A3, A7, JORDAN4: 8;

          then

           A19: (m + 1) <= ( len ( mid (f,i,j))) by A18, NAT_1: 13;

          

           A20: 1 <= m by NAT_1: 11;

          ((m + i) -' 1) = ((((l -' i) + i) + 1) -' 1)

          .= ((l + 1) -' 1) by A15, XREAL_1: 235

          .= l by NAT_D: 34;

          then x = ( LSeg (( mid (f,i,j)),m)) by A1, A3, A7, A14, A20, A18, JORDAN4: 19;

          hence thesis by A20, A19;

        end;

        hence thesis;

      end;

    end;

    theorem :: SPRECT_2:15

    

     Th15: for f be FinSequence of ( TOP-REAL 2) holds ( dom ( X_axis f)) = ( dom f)

    proof

      let f be FinSequence of ( TOP-REAL 2);

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

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: SPRECT_2:16

    

     Th16: for f be FinSequence of ( TOP-REAL 2) holds ( dom ( Y_axis f)) = ( dom f)

    proof

      let f be FinSequence of ( TOP-REAL 2);

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

      hence thesis by FINSEQ_3: 29;

    end;

    reserve r for Real;

    theorem :: SPRECT_2:17

    

     Th17: for a,b,c be Point of ( TOP-REAL 2) st b in ( LSeg (a,c)) & (a `1 ) <= (b `1 ) & (c `1 ) <= (b `1 ) holds a = b or b = c or (a `1 ) = (b `1 ) & (c `1 ) = (b `1 )

    proof

      let a,b,c be Point of ( TOP-REAL 2) such that

       A1: b in ( LSeg (a,c)) and

       A2: (a `1 ) <= (b `1 ) & (c `1 ) <= (b `1 );

      consider r such that

       A3: b = (((1 - r) * a) + (r * c)) and 0 <= r and r <= 1 by A1;

      per cases by A2, XXREAL_0: 1;

        suppose that

         A4: (a `1 ) = (b `1 ) and

         A5: (c `1 ) < (b `1 );

        ((b `1 ) + 0 ) = ((((1 - r) * a) `1 ) + ((r * c) `1 )) by A3, TOPREAL3: 2

        .= ((((1 - r) * a) `1 ) + (r * (c `1 ))) by TOPREAL3: 4

        .= (((1 - r) * (b `1 )) + (r * (c `1 ))) by A4, TOPREAL3: 4

        .= ((b `1 ) + ((r * (c `1 )) - (r * (b `1 ))));

        then

         A6: 0 = (r * ((c `1 ) - (b `1 )));

        ((c `1 ) - (b `1 )) < 0 by A5, XREAL_1: 49;

        then r = 0 by A6, XCMPLX_1: 6;

        

        then b = ((1 * a) + ( 0. ( TOP-REAL 2))) by A3, RLVECT_1: 10

        .= (1 * a) by RLVECT_1: 4

        .= a by RLVECT_1:def 8;

        hence thesis;

      end;

        suppose that

         A7: (a `1 ) < (b `1 ) and

         A8: (c `1 ) = (b `1 );

        (b `1 ) = ((((1 - r) * a) `1 ) + ((r * c) `1 )) by A3, TOPREAL3: 2

        .= ((((1 - r) * a) `1 ) + (r * (c `1 ))) by TOPREAL3: 4

        .= (((1 - r) * (a `1 )) + (r * (b `1 ))) by A8, TOPREAL3: 4;

        then

         A9: 0 = ((1 - r) * ((a `1 ) - (b `1 )));

        ((a `1 ) - (b `1 )) < 0 by A7, XREAL_1: 49;

        then (1 - r) = 0 by A9, XCMPLX_1: 6;

        

        then b = (( 0. ( TOP-REAL 2)) + (1 * c)) by A3, RLVECT_1: 10

        .= (1 * c) by RLVECT_1: 4

        .= c by RLVECT_1:def 8;

        hence thesis;

      end;

        suppose that

         A10: (a `1 ) < (b `1 ) & (c `1 ) < (b `1 );

        (a `1 ) <= (c `1 ) or (c `1 ) <= (a `1 );

        hence thesis by A1, A10, TOPREAL1: 3;

      end;

        suppose (a `1 ) = (b `1 ) & (c `1 ) = (b `1 );

        hence thesis;

      end;

    end;

    theorem :: SPRECT_2:18

    

     Th18: for a,b,c be Point of ( TOP-REAL 2) st b in ( LSeg (a,c)) & (a `2 ) <= (b `2 ) & (c `2 ) <= (b `2 ) holds a = b or b = c or (a `2 ) = (b `2 ) & (c `2 ) = (b `2 )

    proof

      let a,b,c be Point of ( TOP-REAL 2) such that

       A1: b in ( LSeg (a,c)) and

       A2: (a `2 ) <= (b `2 ) & (c `2 ) <= (b `2 );

      consider r such that

       A3: b = (((1 - r) * a) + (r * c)) and 0 <= r and r <= 1 by A1;

      per cases by A2, XXREAL_0: 1;

        suppose that

         A4: (a `2 ) = (b `2 ) and

         A5: (c `2 ) < (b `2 );

        ((b `2 ) + 0 ) = ((((1 - r) * a) `2 ) + ((r * c) `2 )) by A3, TOPREAL3: 2

        .= ((((1 - r) * a) `2 ) + (r * (c `2 ))) by TOPREAL3: 4

        .= (((1 - r) * (b `2 )) + (r * (c `2 ))) by A4, TOPREAL3: 4

        .= ((b `2 ) + ((r * (c `2 )) - (r * (b `2 ))));

        then

         A6: 0 = (r * ((c `2 ) - (b `2 )));

        ((c `2 ) - (b `2 )) < 0 by A5, XREAL_1: 49;

        then r = 0 by A6, XCMPLX_1: 6;

        

        then b = ((1 * a) + ( 0. ( TOP-REAL 2))) by A3, RLVECT_1: 10

        .= (1 * a) by RLVECT_1: 4

        .= a by RLVECT_1:def 8;

        hence thesis;

      end;

        suppose that

         A7: (a `2 ) < (b `2 ) and

         A8: (c `2 ) = (b `2 );

        (b `2 ) = ((((1 - r) * a) `2 ) + ((r * c) `2 )) by A3, TOPREAL3: 2

        .= ((((1 - r) * a) `2 ) + (r * (c `2 ))) by TOPREAL3: 4

        .= (((1 - r) * (a `2 )) + (r * (b `2 ))) by A8, TOPREAL3: 4;

        then

         A9: 0 = ((1 - r) * ((a `2 ) - (b `2 )));

        ((a `2 ) - (b `2 )) < 0 by A7, XREAL_1: 49;

        then (1 - r) = 0 by A9, XCMPLX_1: 6;

        

        then b = (( 0. ( TOP-REAL 2)) + (1 * c)) by A3, RLVECT_1: 10

        .= (1 * c) by RLVECT_1: 4

        .= c by RLVECT_1:def 8;

        hence thesis;

      end;

        suppose that

         A10: (a `2 ) < (b `2 ) & (c `2 ) < (b `2 );

        (a `2 ) <= (c `2 ) or (c `2 ) <= (a `2 );

        hence thesis by A1, A10, TOPREAL1: 4;

      end;

        suppose (a `2 ) = (b `2 ) & (c `2 ) = (b `2 );

        hence thesis;

      end;

    end;

    theorem :: SPRECT_2:19

    

     Th19: for a,b,c be Point of ( TOP-REAL 2) st b in ( LSeg (a,c)) & (a `1 ) >= (b `1 ) & (c `1 ) >= (b `1 ) holds a = b or b = c or (a `1 ) = (b `1 ) & (c `1 ) = (b `1 )

    proof

      let a,b,c be Point of ( TOP-REAL 2) such that

       A1: b in ( LSeg (a,c)) and

       A2: (a `1 ) >= (b `1 ) & (c `1 ) >= (b `1 );

      consider r such that

       A3: b = (((1 - r) * a) + (r * c)) and 0 <= r and r <= 1 by A1;

      per cases by A2, XXREAL_0: 1;

        suppose that

         A4: (a `1 ) = (b `1 ) and

         A5: (c `1 ) > (b `1 );

        ((b `1 ) + 0 ) = ((((1 - r) * a) `1 ) + ((r * c) `1 )) by A3, TOPREAL3: 2

        .= ((((1 - r) * a) `1 ) + (r * (c `1 ))) by TOPREAL3: 4

        .= (((1 - r) * (b `1 )) + (r * (c `1 ))) by A4, TOPREAL3: 4

        .= ((b `1 ) + ((r * (c `1 )) - (r * (b `1 ))));

        then

         A6: 0 = (r * ((c `1 ) - (b `1 )));

        ((c `1 ) - (b `1 )) > 0 by A5, XREAL_1: 50;

        then r = 0 by A6, XCMPLX_1: 6;

        

        then b = ((1 * a) + ( 0. ( TOP-REAL 2))) by A3, RLVECT_1: 10

        .= (1 * a) by RLVECT_1: 4

        .= a by RLVECT_1:def 8;

        hence thesis;

      end;

        suppose that

         A7: (a `1 ) > (b `1 ) and

         A8: (c `1 ) = (b `1 );

        (b `1 ) = ((((1 - r) * a) `1 ) + ((r * c) `1 )) by A3, TOPREAL3: 2

        .= ((((1 - r) * a) `1 ) + (r * (c `1 ))) by TOPREAL3: 4

        .= (((1 - r) * (a `1 )) + (r * (b `1 ))) by A8, TOPREAL3: 4;

        then

         A9: 0 = ((1 - r) * ((a `1 ) - (b `1 )));

        ((a `1 ) - (b `1 )) > 0 by A7, XREAL_1: 50;

        then (1 - r) = 0 by A9, XCMPLX_1: 6;

        

        then b = (( 0. ( TOP-REAL 2)) + (1 * c)) by A3, RLVECT_1: 10

        .= (1 * c) by RLVECT_1: 4

        .= c by RLVECT_1:def 8;

        hence thesis;

      end;

        suppose that

         A10: (a `1 ) > (b `1 ) & (c `1 ) > (b `1 );

        (a `1 ) >= (c `1 ) or (c `1 ) >= (a `1 );

        hence thesis by A1, A10, TOPREAL1: 3;

      end;

        suppose (a `1 ) = (b `1 ) & (c `1 ) = (b `1 );

        hence thesis;

      end;

    end;

    theorem :: SPRECT_2:20

    

     Th20: for a,b,c be Point of ( TOP-REAL 2) st b in ( LSeg (a,c)) & (a `2 ) >= (b `2 ) & (c `2 ) >= (b `2 ) holds a = b or b = c or (a `2 ) = (b `2 ) & (c `2 ) = (b `2 )

    proof

      let a,b,c be Point of ( TOP-REAL 2) such that

       A1: b in ( LSeg (a,c)) and

       A2: (a `2 ) >= (b `2 ) & (c `2 ) >= (b `2 );

      consider r such that

       A3: b = (((1 - r) * a) + (r * c)) and 0 <= r and r <= 1 by A1;

      per cases by A2, XXREAL_0: 1;

        suppose that

         A4: (a `2 ) = (b `2 ) and

         A5: (c `2 ) > (b `2 );

        ((b `2 ) + 0 ) = ((((1 - r) * a) `2 ) + ((r * c) `2 )) by A3, TOPREAL3: 2

        .= ((((1 - r) * a) `2 ) + (r * (c `2 ))) by TOPREAL3: 4

        .= (((1 - r) * (b `2 )) + (r * (c `2 ))) by A4, TOPREAL3: 4

        .= ((b `2 ) + ((r * (c `2 )) - (r * (b `2 ))));

        then

         A6: 0 = (r * ((c `2 ) - (b `2 )));

        ((c `2 ) - (b `2 )) > 0 by A5, XREAL_1: 50;

        then r = 0 by A6, XCMPLX_1: 6;

        

        then b = ((1 * a) + ( 0. ( TOP-REAL 2))) by A3, RLVECT_1: 10

        .= (1 * a) by RLVECT_1: 4

        .= a by RLVECT_1:def 8;

        hence thesis;

      end;

        suppose that

         A7: (a `2 ) > (b `2 ) and

         A8: (c `2 ) = (b `2 );

        (b `2 ) = ((((1 - r) * a) `2 ) + ((r * c) `2 )) by A3, TOPREAL3: 2

        .= ((((1 - r) * a) `2 ) + (r * (c `2 ))) by TOPREAL3: 4

        .= (((1 - r) * (a `2 )) + (r * (b `2 ))) by A8, TOPREAL3: 4;

        then

         A9: 0 = ((1 - r) * ((a `2 ) - (b `2 )));

        ((a `2 ) - (b `2 )) > 0 by A7, XREAL_1: 50;

        then (1 - r) = 0 by A9, XCMPLX_1: 6;

        

        then b = (( 0. ( TOP-REAL 2)) + (1 * c)) by A3, RLVECT_1: 10

        .= (1 * c) by RLVECT_1: 4

        .= c by RLVECT_1:def 8;

        hence thesis;

      end;

        suppose that

         A10: (a `2 ) > (b `2 ) & (c `2 ) > (b `2 );

        (a `2 ) >= (c `2 ) or (c `2 ) >= (a `2 );

        hence thesis by A1, A10, TOPREAL1: 4;

      end;

        suppose (a `2 ) = (b `2 ) & (c `2 ) = (b `2 );

        hence thesis;

      end;

    end;

    begin

    definition

      let f,g be FinSequence of ( TOP-REAL 2);

      :: SPRECT_2:def1

      pred g is_in_the_area_of f means for n st n in ( dom g) holds ( W-bound ( L~ f)) <= ((g /. n) `1 ) & ((g /. n) `1 ) <= ( E-bound ( L~ f)) & ( S-bound ( L~ f)) <= ((g /. n) `2 ) & ((g /. n) `2 ) <= ( N-bound ( L~ f));

    end

    theorem :: SPRECT_2:21

    

     Th21: for f be non trivial FinSequence of ( TOP-REAL 2) holds f is_in_the_area_of f

    proof

      let f be non trivial FinSequence of ( TOP-REAL 2);

      let n;

      assume

       A1: n in ( dom f);

      ( len f) >= 2 by NAT_D: 60;

      then (f /. n) in ( L~ f) by A1, GOBOARD1: 1;

      hence thesis by PSCOMP_1: 24;

    end;

    theorem :: SPRECT_2:22

    

     Th22: for f,g be FinSequence of ( TOP-REAL 2) st g is_in_the_area_of f holds for i, j st i in ( dom g) & j in ( dom g) holds ( mid (g,i,j)) is_in_the_area_of f

    proof

      let f,g be FinSequence of ( TOP-REAL 2) such that

       A1: for n st n in ( dom g) holds ( W-bound ( L~ f)) <= ((g /. n) `1 ) & ((g /. n) `1 ) <= ( E-bound ( L~ f)) & ( S-bound ( L~ f)) <= ((g /. n) `2 ) & ((g /. n) `2 ) <= ( N-bound ( L~ f));

      let i, j such that

       A2: i in ( dom g) & j in ( dom g);

      set h = ( mid (g,i,j));

      per cases ;

        suppose

         A3: i <= j;

        let n;

        assume n in ( dom h);

        then ((n + i) -' 1) in ( dom g) & (h /. n) = (g /. ((n + i) -' 1)) by A2, A3, Th1, Th3;

        hence thesis by A1;

      end;

        suppose

         A4: i > j;

        let n;

        assume n in ( dom h);

        then ((i -' n) + 1) in ( dom g) & (h /. n) = (g /. ((i -' n) + 1)) by A2, A4, Th2, Th4;

        hence thesis by A1;

      end;

    end;

    theorem :: SPRECT_2:23

    for f be non trivial FinSequence of ( TOP-REAL 2) holds for i, j st i in ( dom f) & j in ( dom f) holds ( mid (f,i,j)) is_in_the_area_of f by Th21, Th22;

    theorem :: SPRECT_2:24

    

     Th24: for f,g,h be FinSequence of ( TOP-REAL 2) st g is_in_the_area_of f & h is_in_the_area_of f holds (g ^ h) is_in_the_area_of f

    proof

      let f,g,h be FinSequence of ( TOP-REAL 2) such that

       A1: g is_in_the_area_of f and

       A2: h is_in_the_area_of f;

      let n;

      assume

       A3: n in ( dom (g ^ h));

      per cases by A3, FINSEQ_1: 25;

        suppose

         A4: n in ( dom g);

        then ((g ^ h) /. n) = (g /. n) by FINSEQ_4: 68;

        hence thesis by A1, A4;

      end;

        suppose ex i be Nat st i in ( dom h) & n = (( len g) + i);

        then

        consider i be Nat such that

         A5: i in ( dom h) and

         A6: n = (( len g) + i);

        ((g ^ h) /. n) = (h /. i) by A5, A6, FINSEQ_4: 69;

        hence thesis by A2, A5;

      end;

    end;

    theorem :: SPRECT_2:25

    

     Th25: for f be non trivial FinSequence of ( TOP-REAL 2) holds <*( NE-corner ( L~ f))*> is_in_the_area_of f

    proof

      let f be non trivial FinSequence of ( TOP-REAL 2);

      set g = <*( NE-corner ( L~ f))*>;

      let n;

      assume

       A1: n in ( dom g);

      ( dom g) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      then n = 1 by A1, TARSKI:def 1;

      then (g /. n) = |[( E-bound ( L~ f)), ( N-bound ( L~ f))]| by FINSEQ_4: 16;

      then ((g /. n) `1 ) = ( E-bound ( L~ f)) & ((g /. n) `2 ) = ( N-bound ( L~ f)) by EUCLID: 52;

      hence thesis by SPRECT_1: 21, SPRECT_1: 22;

    end;

    theorem :: SPRECT_2:26

    

     Th26: for f be non trivial FinSequence of ( TOP-REAL 2) holds <*( NW-corner ( L~ f))*> is_in_the_area_of f

    proof

      let f be non trivial FinSequence of ( TOP-REAL 2);

      set g = <*( NW-corner ( L~ f))*>;

      let n;

      assume

       A1: n in ( dom g);

      ( dom g) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      then n = 1 by A1, TARSKI:def 1;

      then (g /. n) = |[( W-bound ( L~ f)), ( N-bound ( L~ f))]| by FINSEQ_4: 16;

      then ((g /. n) `1 ) = ( W-bound ( L~ f)) & ((g /. n) `2 ) = ( N-bound ( L~ f)) by EUCLID: 52;

      hence thesis by SPRECT_1: 21, SPRECT_1: 22;

    end;

    theorem :: SPRECT_2:27

    

     Th27: for f be non trivial FinSequence of ( TOP-REAL 2) holds <*( SE-corner ( L~ f))*> is_in_the_area_of f

    proof

      let f be non trivial FinSequence of ( TOP-REAL 2);

      set g = <*( SE-corner ( L~ f))*>;

      let n;

      assume

       A1: n in ( dom g);

      ( dom g) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      then n = 1 by A1, TARSKI:def 1;

      then (g /. n) = |[( E-bound ( L~ f)), ( S-bound ( L~ f))]| by FINSEQ_4: 16;

      then ((g /. n) `1 ) = ( E-bound ( L~ f)) & ((g /. n) `2 ) = ( S-bound ( L~ f)) by EUCLID: 52;

      hence thesis by SPRECT_1: 21, SPRECT_1: 22;

    end;

    theorem :: SPRECT_2:28

    

     Th28: for f be non trivial FinSequence of ( TOP-REAL 2) holds <*( SW-corner ( L~ f))*> is_in_the_area_of f

    proof

      let f be non trivial FinSequence of ( TOP-REAL 2);

      set g = <*( SW-corner ( L~ f))*>;

      let n;

      assume

       A1: n in ( dom g);

      ( dom g) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      then n = 1 by A1, TARSKI:def 1;

      then (g /. n) = |[( W-bound ( L~ f)), ( S-bound ( L~ f))]| by FINSEQ_4: 16;

      then ((g /. n) `1 ) = ( W-bound ( L~ f)) & ((g /. n) `2 ) = ( S-bound ( L~ f)) by EUCLID: 52;

      hence thesis by SPRECT_1: 21, SPRECT_1: 22;

    end;

    begin

    definition

      let f,g be FinSequence of ( TOP-REAL 2);

      :: SPRECT_2:def2

      pred g is_a_h.c._for f means g is_in_the_area_of f & ((g /. 1) `1 ) = ( W-bound ( L~ f)) & ((g /. ( len g)) `1 ) = ( E-bound ( L~ f));

      :: SPRECT_2:def3

      pred g is_a_v.c._for f means g is_in_the_area_of f & ((g /. 1) `2 ) = ( S-bound ( L~ f)) & ((g /. ( len g)) `2 ) = ( N-bound ( L~ f));

    end

    theorem :: SPRECT_2:29

    

     Th29: for f be FinSequence of ( TOP-REAL 2), g,h be one-to-one special FinSequence of ( TOP-REAL 2) st 2 <= ( len g) & 2 <= ( len h) & g is_a_h.c._for f & h is_a_v.c._for f holds ( L~ g) meets ( L~ h)

    proof

      let f be FinSequence of ( TOP-REAL 2), g,h be one-to-one special FinSequence of ( TOP-REAL 2) such that

       A1: 2 <= ( len g) & 2 <= ( len h) and

       A2: for n st n in ( dom g) holds ( W-bound ( L~ f)) <= ((g /. n) `1 ) & ((g /. n) `1 ) <= ( E-bound ( L~ f)) & ( S-bound ( L~ f)) <= ((g /. n) `2 ) & ((g /. n) `2 ) <= ( N-bound ( L~ f)) and

       A3: ((g /. 1) `1 ) = ( W-bound ( L~ f)) and

       A4: ((g /. ( len g)) `1 ) = ( E-bound ( L~ f)) and

       A5: for n st n in ( dom h) holds ( W-bound ( L~ f)) <= ((h /. n) `1 ) & ((h /. n) `1 ) <= ( E-bound ( L~ f)) & ( S-bound ( L~ f)) <= ((h /. n) `2 ) & ((h /. n) `2 ) <= ( N-bound ( L~ f)) and

       A6: ((h /. 1) `2 ) = ( S-bound ( L~ f)) and

       A7: ((h /. ( len h)) `2 ) = ( N-bound ( L~ f));

      reconsider g, h as non empty one-to-one special FinSequence of ( TOP-REAL 2) by A1, CARD_1: 27;

      

       A8: ( X_axis h) lies_between ((( X_axis g) . 1),(( X_axis g) . ( len g)))

      proof

        let n;

        set F = ( X_axis g), r = (( X_axis g) . 1), s = (( X_axis g) . ( len g)), H = ( X_axis h);

        assume n in ( dom H);

        then

         A9: n in ( dom h) & (H . n) = ((h /. n) `1 ) by Th15, GOBOARD1:def 1;

        1 in ( dom F) by FINSEQ_5: 6;

        then r = ( W-bound ( L~ f)) by A3, GOBOARD1:def 1;

        hence r <= (H . n) by A5, A9;

        ( len F) = ( len g) & ( len F) in ( dom F) by FINSEQ_5: 6, GOBOARD1:def 1;

        then s = ( E-bound ( L~ f)) by A4, GOBOARD1:def 1;

        hence thesis by A5, A9;

      end;

      

       A10: ( Y_axis h) lies_between ((( Y_axis h) . 1),(( Y_axis h) . ( len h)))

      proof

        let n;

        set F = ( Y_axis h), r = (( Y_axis h) . 1), s = (( Y_axis h) . ( len h));

        assume n in ( dom F);

        then

         A11: n in ( dom h) & (F . n) = ((h /. n) `2 ) by Th16, GOBOARD1:def 2;

        1 in ( dom F) by FINSEQ_5: 6;

        then r = ( S-bound ( L~ f)) by A6, GOBOARD1:def 2;

        hence r <= (F . n) by A5, A11;

        ( len F) = ( len h) & ( len F) in ( dom F) by FINSEQ_5: 6, GOBOARD1:def 2;

        then s = ( N-bound ( L~ f)) by A7, GOBOARD1:def 2;

        hence thesis by A5, A11;

      end;

      

       A12: ( Y_axis g) lies_between ((( Y_axis h) . 1),(( Y_axis h) . ( len h)))

      proof

        let n;

        set F = ( Y_axis h), r = (( Y_axis h) . 1), s = (( Y_axis h) . ( len h)), G = ( Y_axis g);

        assume n in ( dom G);

        then

         A13: n in ( dom g) & (G . n) = ((g /. n) `2 ) by Th16, GOBOARD1:def 2;

        1 in ( dom F) by FINSEQ_5: 6;

        then r = ( S-bound ( L~ f)) by A6, GOBOARD1:def 2;

        hence r <= (G . n) by A2, A13;

        ( len F) = ( len h) & ( len F) in ( dom F) by FINSEQ_5: 6, GOBOARD1:def 2;

        then s = ( N-bound ( L~ f)) by A7, GOBOARD1:def 2;

        hence thesis by A2, A13;

      end;

      ( X_axis g) lies_between ((( X_axis g) . 1),(( X_axis g) . ( len g)))

      proof

        let n;

        set F = ( X_axis g), r = (( X_axis g) . 1), s = (( X_axis g) . ( len g));

        assume n in ( dom F);

        then

         A14: n in ( dom g) & (F . n) = ((g /. n) `1 ) by Th15, GOBOARD1:def 1;

        1 in ( dom F) by FINSEQ_5: 6;

        then r = ( W-bound ( L~ f)) by A3, GOBOARD1:def 1;

        hence r <= (F . n) by A2, A14;

        ( len F) = ( len g) & ( len F) in ( dom F) by FINSEQ_5: 6, GOBOARD1:def 1;

        then s = ( E-bound ( L~ f)) by A4, GOBOARD1:def 1;

        hence thesis by A2, A14;

      end;

      hence thesis by A1, A8, A12, A10, GOBOARD4: 5;

    end;

    begin

    definition

      let f be FinSequence of ( TOP-REAL 2);

      :: SPRECT_2:def4

      attr f is clockwise_oriented means (( Rotate (f,( N-min ( L~ f)))) /. 2) in ( N-most ( L~ f));

    end

    theorem :: SPRECT_2:30

    

     Th30: for f be non constant standard special_circular_sequence st (f /. 1) = ( N-min ( L~ f)) holds f is clockwise_oriented iff (f /. 2) in ( N-most ( L~ f)) by FINSEQ_6: 89;

    registration

      cluster R^2-unit_square -> compact;

      coherence by TOPREAL2: 2;

    end

    theorem :: SPRECT_2:31

    

     Th31: ( N-bound R^2-unit_square ) = 1

    proof

      set X = R^2-unit_square ;

      reconsider Z = (( proj2 | X) .: the carrier of (( TOP-REAL 2) | X)) as Subset of REAL ;

      

       A1: X = ( [#] (( TOP-REAL 2) | X)) by PRE_TOPC:def 5

      .= the carrier of (( TOP-REAL 2) | X);

      

       A2: for q be Real st for p be Real st p in Z holds p <= q holds 1 <= q

      proof

        let q be Real such that

         A3: for p be Real st p in Z holds p <= q;

         |[1, 1]| in ( LSeg ( |[1, 0 ]|, |[1, 1]|)) by RLTOPSP1: 68;

        then |[1, 1]| in (( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) \/ ( LSeg ( |[1, 0 ]|, |[1, 1]|))) by XBOOLE_0:def 3;

        then

         A4: |[1, 1]| in X by XBOOLE_0:def 3;

        

        then (( proj2 | X) . |[1, 1]|) = ( |[1, 1]| `2 ) by PSCOMP_1: 23

        .= 1 by EUCLID: 52;

        hence thesis by A1, A3, A4, FUNCT_2: 35;

      end;

      for p be Real st p in Z holds p <= 1

      proof

        let p be Real;

        assume p in Z;

        then

        consider p0 be object such that

         A5: p0 in the carrier of (( TOP-REAL 2) | X) and p0 in the carrier of (( TOP-REAL 2) | X) and

         A6: p = (( proj2 | X) . p0) by FUNCT_2: 64;

        reconsider p0 as Point of ( TOP-REAL 2) by A1, A5;

        ex q be Point of ( TOP-REAL 2) st p0 = q & ((q `1 ) = 0 & (q `2 ) <= 1 & (q `2 ) >= 0 or (q `1 ) <= 1 & (q `1 ) >= 0 & (q `2 ) = 1 or (q `1 ) <= 1 & (q `1 ) >= 0 & (q `2 ) = 0 or (q `1 ) = 1 & (q `2 ) <= 1 & (q `2 ) >= 0 ) by A1, A5, TOPREAL1: 14;

        hence thesis by A1, A5, A6, PSCOMP_1: 23;

      end;

      hence thesis by A2, SEQ_4: 46;

    end;

    theorem :: SPRECT_2:32

    

     Th32: ( W-bound R^2-unit_square ) = 0

    proof

      set X = R^2-unit_square ;

      reconsider Z = (( proj1 | X) .: the carrier of (( TOP-REAL 2) | X)) as Subset of REAL ;

      

       A1: X = ( [#] (( TOP-REAL 2) | X)) by PRE_TOPC:def 5

      .= the carrier of (( TOP-REAL 2) | X);

      

       A2: for q be Real st for p be Real st p in Z holds p >= q holds 0 >= q

      proof

        let q be Real such that

         A3: for p be Real st p in Z holds p >= q;

         |[ 0 , 0 ]| in ( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) by RLTOPSP1: 68;

        then |[ 0 , 0 ]| in (( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) \/ ( LSeg ( |[1, 0 ]|, |[1, 1]|))) by XBOOLE_0:def 3;

        then

         A4: |[ 0 , 0 ]| in X by XBOOLE_0:def 3;

        

        then (( proj1 | X) . |[ 0 , 0 ]|) = ( |[ 0 , 0 ]| `1 ) by PSCOMP_1: 22

        .= 0 by EUCLID: 52;

        hence thesis by A1, A3, A4, FUNCT_2: 35;

      end;

      for p be Real st p in Z holds p >= 0

      proof

        let p be Real;

        assume p in Z;

        then

        consider p0 be object such that

         A5: p0 in the carrier of (( TOP-REAL 2) | X) and p0 in the carrier of (( TOP-REAL 2) | X) and

         A6: p = (( proj1 | X) . p0) by FUNCT_2: 64;

        reconsider p0 as Point of ( TOP-REAL 2) by A1, A5;

        ex q be Point of ( TOP-REAL 2) st p0 = q & ((q `1 ) = 0 & (q `2 ) <= 1 & (q `2 ) >= 0 or (q `1 ) <= 1 & (q `1 ) >= 0 & (q `2 ) = 1 or (q `1 ) <= 1 & (q `1 ) >= 0 & (q `2 ) = 0 or (q `1 ) = 1 & (q `2 ) <= 1 & (q `2 ) >= 0 ) by A1, A5, TOPREAL1: 14;

        hence thesis by A1, A5, A6, PSCOMP_1: 22;

      end;

      hence thesis by A2, SEQ_4: 44;

    end;

    theorem :: SPRECT_2:33

    

     Th33: ( E-bound R^2-unit_square ) = 1

    proof

      set X = R^2-unit_square ;

      reconsider Z = (( proj1 | X) .: the carrier of (( TOP-REAL 2) | X)) as Subset of REAL ;

      

       A1: X = ( [#] (( TOP-REAL 2) | X)) by PRE_TOPC:def 5

      .= the carrier of (( TOP-REAL 2) | X);

      

       A2: for q be Real st for p be Real st p in Z holds p <= q holds 1 <= q

      proof

        let q be Real such that

         A3: for p be Real st p in Z holds p <= q;

         |[1, 1]| in ( LSeg ( |[1, 0 ]|, |[1, 1]|)) by RLTOPSP1: 68;

        then |[1, 1]| in (( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) \/ ( LSeg ( |[1, 0 ]|, |[1, 1]|))) by XBOOLE_0:def 3;

        then

         A4: |[1, 1]| in X by XBOOLE_0:def 3;

        

        then (( proj1 | X) . |[1, 1]|) = ( |[1, 1]| `1 ) by PSCOMP_1: 22

        .= 1 by EUCLID: 52;

        hence thesis by A1, A3, A4, FUNCT_2: 35;

      end;

      for p be Real st p in Z holds p <= 1

      proof

        let p be Real;

        assume p in Z;

        then

        consider p0 be object such that

         A5: p0 in the carrier of (( TOP-REAL 2) | X) and p0 in the carrier of (( TOP-REAL 2) | X) and

         A6: p = (( proj1 | X) . p0) by FUNCT_2: 64;

        reconsider p0 as Point of ( TOP-REAL 2) by A1, A5;

        ex q be Point of ( TOP-REAL 2) st p0 = q & ((q `1 ) = 0 & (q `2 ) <= 1 & (q `2 ) >= 0 or (q `1 ) <= 1 & (q `1 ) >= 0 & (q `2 ) = 1 or (q `1 ) <= 1 & (q `1 ) >= 0 & (q `2 ) = 0 or (q `1 ) = 1 & (q `2 ) <= 1 & (q `2 ) >= 0 ) by A1, A5, TOPREAL1: 14;

        hence thesis by A1, A5, A6, PSCOMP_1: 22;

      end;

      hence thesis by A2, SEQ_4: 46;

    end;

    theorem :: SPRECT_2:34

    ( S-bound R^2-unit_square ) = 0

    proof

      set X = R^2-unit_square ;

      reconsider Z = (( proj2 | X) .: the carrier of (( TOP-REAL 2) | X)) as Subset of REAL ;

      

       A1: X = ( [#] (( TOP-REAL 2) | X)) by PRE_TOPC:def 5

      .= the carrier of (( TOP-REAL 2) | X);

      

       A2: for q be Real st for p be Real st p in Z holds p >= q holds 0 >= q

      proof

        let q be Real such that

         A3: for p be Real st p in Z holds p >= q;

         |[1, 0 ]| in ( LSeg ( |[1, 0 ]|, |[1, 1]|)) by RLTOPSP1: 68;

        then |[1, 0 ]| in (( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) \/ ( LSeg ( |[1, 0 ]|, |[1, 1]|))) by XBOOLE_0:def 3;

        then

         A4: |[1, 0 ]| in X by XBOOLE_0:def 3;

        

        then (( proj2 | X) . |[1, 0 ]|) = ( |[1, 0 ]| `2 ) by PSCOMP_1: 23

        .= 0 by EUCLID: 52;

        hence thesis by A1, A3, A4, FUNCT_2: 35;

      end;

      for p be Real st p in Z holds p >= 0

      proof

        let p be Real;

        assume p in Z;

        then

        consider p0 be object such that

         A5: p0 in the carrier of (( TOP-REAL 2) | X) and p0 in the carrier of (( TOP-REAL 2) | X) and

         A6: p = (( proj2 | X) . p0) by FUNCT_2: 64;

        reconsider p0 as Point of ( TOP-REAL 2) by A1, A5;

        ex q be Point of ( TOP-REAL 2) st p0 = q & ((q `1 ) = 0 & (q `2 ) <= 1 & (q `2 ) >= 0 or (q `1 ) <= 1 & (q `1 ) >= 0 & (q `2 ) = 1 or (q `1 ) <= 1 & (q `1 ) >= 0 & (q `2 ) = 0 or (q `1 ) = 1 & (q `2 ) <= 1 & (q `2 ) >= 0 ) by A1, A5, TOPREAL1: 14;

        hence thesis by A1, A5, A6, PSCOMP_1: 23;

      end;

      hence thesis by A2, SEQ_4: 44;

    end;

    theorem :: SPRECT_2:35

    

     Th35: ( N-most R^2-unit_square ) = ( LSeg ( |[ 0 , 1]|, |[1, 1]|))

    proof

      set X = R^2-unit_square ;

      (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) \/ ( LSeg ( |[ 0 , 1]|, |[1, 1]|))) c= X & ( LSeg ( |[ 0 , 1]|, |[1, 1]|)) c= (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) \/ ( LSeg ( |[ 0 , 1]|, |[1, 1]|))) by XBOOLE_1: 7;

      hence thesis by Th31, Th32, Th33, XBOOLE_1: 1, XBOOLE_1: 28;

    end;

    theorem :: SPRECT_2:36

    ( N-min R^2-unit_square ) = |[ 0 , 1]|

    proof

      ( lower_bound ( proj1 | ( LSeg ( |[ 0 , 1]|, |[1, 1]|)))) = 0

      proof

        set X = ( LSeg ( |[ 0 , 1]|, |[1, 1]|));

        reconsider Z = (( proj1 | X) .: the carrier of (( TOP-REAL 2) | X)) as Subset of REAL ;

        

         A1: X = ( [#] (( TOP-REAL 2) | X)) by PRE_TOPC:def 5

        .= the carrier of (( TOP-REAL 2) | X);

        

         A2: for p be Real st p in Z holds p >= 0

        proof

          let p be Real;

          assume p in Z;

          then

          consider p0 be object such that

           A3: p0 in the carrier of (( TOP-REAL 2) | X) and p0 in the carrier of (( TOP-REAL 2) | X) and

           A4: p = (( proj1 | X) . p0) by FUNCT_2: 64;

          reconsider p0 as Point of ( TOP-REAL 2) by A1, A3;

          ( |[ 0 , 1]| `1 ) = 0 & ( |[1, 1]| `1 ) = 1 by EUCLID: 52;

          then (p0 `1 ) >= 0 by A1, A3, TOPREAL1: 3;

          hence thesis by A1, A3, A4, PSCOMP_1: 22;

        end;

        for q be Real st for p be Real st p in Z holds p >= q holds 0 >= q

        proof

          

           A5: (( proj1 | X) . |[ 0 , 1]|) = ( |[ 0 , 1]| `1 ) by PSCOMP_1: 22, RLTOPSP1: 68

          .= 0 by EUCLID: 52;

          

           A6: |[ 0 , 1]| in X by RLTOPSP1: 68;

          let q be Real;

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

          hence thesis by A1, A6, A5, FUNCT_2: 35;

        end;

        hence thesis by A2, SEQ_4: 44;

      end;

      hence thesis by Th31, Th35;

    end;

    registration

      let X be non vertical non horizontal non empty compact Subset of ( TOP-REAL 2);

      cluster ( SpStSeq X) -> clockwise_oriented;

      coherence

      proof

        set f = ( SpStSeq X);

        (f /. 2) = ( N-max ( L~ f)) by SPRECT_1: 84;

        then (f /. 1) = ( N-min ( L~ f)) & (f /. 2) in ( N-most ( L~ f)) by PSCOMP_1: 42, SPRECT_1: 83;

        hence thesis by Th30;

      end;

    end

    registration

      cluster clockwise_oriented for non constant standard special_circular_sequence;

      existence

      proof

        set X = the non vertical non horizontal non empty compact Subset of ( TOP-REAL 2);

        take ( SpStSeq X);

        thus thesis;

      end;

    end

    theorem :: SPRECT_2:37

    

     Th37: for f be non constant standard special_circular_sequence, i, j st i > j & (1 < j & i <= ( len f) or 1 <= j & i < ( len f)) holds ( mid (f,i,j)) is S-Sequence_in_R2

    proof

      let f be non constant standard special_circular_sequence, i, j such that

       A1: i > j and

       A2: 1 < j & i <= ( len f) or 1 <= j & i < ( len f);

      

       A3: ( Rev ( mid (f,j,i))) = ( mid (f,i,j)) by JORDAN4: 18;

      per cases by A2;

        suppose 1 < j & i <= ( len f);

        then ( mid (f,j,i)) is S-Sequence_in_R2 by A1, JORDAN4: 40;

        hence thesis by A3;

      end;

        suppose

         A4: 1 <= j & i < ( len f);

        then (i + 1) <= ( len f) by NAT_1: 13;

        then ( mid (f,j,i)) is S-Sequence_in_R2 by A1, A4, JORDAN4: 39;

        hence thesis by A3;

      end;

    end;

    theorem :: SPRECT_2:38

    

     Th38: for f be non constant standard special_circular_sequence, i, j st i < j & (1 < i & j <= ( len f) or 1 <= i & j < ( len f)) holds ( mid (f,i,j)) is S-Sequence_in_R2

    proof

      let f be non constant standard special_circular_sequence, i, j;

      assume i < j & (1 < i & j <= ( len f) or 1 <= i & j < ( len f));

      then ( mid (f,j,i)) is S-Sequence_in_R2 by Th37;

      then ( Rev ( Rev ( mid (f,i,j)))) = ( mid (f,i,j)) & ( Rev ( mid (f,i,j))) is S-Sequence_in_R2 by JORDAN4: 18;

      hence thesis;

    end;

    reserve f for non trivial FinSequence of ( TOP-REAL 2);

    theorem :: SPRECT_2:39

    

     Th39: ( N-min ( L~ f)) in ( rng f)

    proof

      set p = ( N-min ( L~ f));

      

       A1: ( len f) >= 2 by NAT_D: 60;

      consider i be Nat such that

       A2: 1 <= i and

       A3: (i + 1) <= ( len f) and

       A4: p in ( LSeg ((f /. i),(f /. (i + 1)))) by SPPOL_2: 14, SPRECT_1: 11;

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

      then

       A5: (i + 1) in ( dom f) by A3, FINSEQ_3: 25;

      then (f /. (i + 1)) in ( L~ f) by A1, GOBOARD1: 1;

      then

       A6: ((f /. (i + 1)) `2 ) <= ( N-bound ( L~ f)) by PSCOMP_1: 24;

      

       A7: (p `2 ) = ( N-bound ( L~ f)) by EUCLID: 52;

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

      then i <= ( len f) by A3, XXREAL_0: 2;

      then

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

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

      then

       A9: ((f /. i) `2 ) <= ( N-bound ( L~ f)) by PSCOMP_1: 24;

      now

        per cases by A4, A9, A6, A7, Th18;

          suppose p = (f /. i);

          hence thesis by A8, PARTFUN2: 2;

        end;

          suppose p = (f /. (i + 1));

          hence thesis by A5, PARTFUN2: 2;

        end;

          suppose

           A10: (p `2 ) = ((f /. i) `2 ) & (p `2 ) = ((f /. (i + 1)) `2 );

          then (f /. (i + 1)) in ( N-most ( L~ f)) by A1, A5, A7, Th10, GOBOARD1: 1;

          then

           A11: ((f /. (i + 1)) `1 ) >= (p `1 ) by PSCOMP_1: 39;

          ((f /. i) `1 ) <= ((f /. (i + 1)) `1 ) or ((f /. (i + 1)) `1 ) <= ((f /. i) `1 );

          then

           A12: ((f /. i) `1 ) <= (p `1 ) or ((f /. (i + 1)) `1 ) <= (p `1 ) by A4, TOPREAL1: 3;

          (f /. i) in ( N-most ( L~ f)) by A1, A8, A7, A10, Th10, GOBOARD1: 1;

          then ((f /. i) `1 ) >= (p `1 ) by PSCOMP_1: 39;

          then (p `1 ) = ((f /. i) `1 ) or (p `1 ) = ((f /. (i + 1)) `1 ) by A11, A12, XXREAL_0: 1;

          then p = (f /. i) or p = (f /. (i + 1)) by A10, TOPREAL3: 6;

          hence thesis by A8, A5, PARTFUN2: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: SPRECT_2:40

    

     Th40: ( N-max ( L~ f)) in ( rng f)

    proof

      set p = ( N-max ( L~ f));

      

       A1: ( len f) >= 2 by NAT_D: 60;

      consider i be Nat such that

       A2: 1 <= i and

       A3: (i + 1) <= ( len f) and

       A4: p in ( LSeg ((f /. i),(f /. (i + 1)))) by SPPOL_2: 14, SPRECT_1: 11;

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

      then

       A5: (i + 1) in ( dom f) by A3, FINSEQ_3: 25;

      then (f /. (i + 1)) in ( L~ f) by A1, GOBOARD1: 1;

      then

       A6: ((f /. (i + 1)) `2 ) <= ( N-bound ( L~ f)) by PSCOMP_1: 24;

      

       A7: (p `2 ) = ( N-bound ( L~ f)) by EUCLID: 52;

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

      then i <= ( len f) by A3, XXREAL_0: 2;

      then

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

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

      then

       A9: ((f /. i) `2 ) <= ( N-bound ( L~ f)) by PSCOMP_1: 24;

      now

        per cases by A4, A9, A6, A7, Th18;

          suppose p = (f /. i);

          hence thesis by A8, PARTFUN2: 2;

        end;

          suppose p = (f /. (i + 1));

          hence thesis by A5, PARTFUN2: 2;

        end;

          suppose

           A10: (p `2 ) = ((f /. i) `2 ) & (p `2 ) = ((f /. (i + 1)) `2 );

          then (f /. (i + 1)) in ( N-most ( L~ f)) by A1, A5, A7, Th10, GOBOARD1: 1;

          then

           A11: ((f /. (i + 1)) `1 ) <= (p `1 ) by PSCOMP_1: 39;

          ((f /. i) `1 ) >= ((f /. (i + 1)) `1 ) or ((f /. (i + 1)) `1 ) >= ((f /. i) `1 );

          then

           A12: ((f /. i) `1 ) >= (p `1 ) or ((f /. (i + 1)) `1 ) >= (p `1 ) by A4, TOPREAL1: 3;

          (f /. i) in ( N-most ( L~ f)) by A1, A8, A7, A10, Th10, GOBOARD1: 1;

          then ((f /. i) `1 ) <= (p `1 ) by PSCOMP_1: 39;

          then (p `1 ) = ((f /. i) `1 ) or (p `1 ) = ((f /. (i + 1)) `1 ) by A11, A12, XXREAL_0: 1;

          then p = (f /. i) or p = (f /. (i + 1)) by A10, TOPREAL3: 6;

          hence thesis by A8, A5, PARTFUN2: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: SPRECT_2:41

    

     Th41: ( S-min ( L~ f)) in ( rng f)

    proof

      set p = ( S-min ( L~ f));

      

       A1: ( len f) >= 2 by NAT_D: 60;

      consider i be Nat such that

       A2: 1 <= i and

       A3: (i + 1) <= ( len f) and

       A4: p in ( LSeg ((f /. i),(f /. (i + 1)))) by SPPOL_2: 14, SPRECT_1: 12;

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

      then

       A5: (i + 1) in ( dom f) by A3, FINSEQ_3: 25;

      then (f /. (i + 1)) in ( L~ f) by A1, GOBOARD1: 1;

      then

       A6: ((f /. (i + 1)) `2 ) >= ( S-bound ( L~ f)) by PSCOMP_1: 24;

      

       A7: (p `2 ) = ( S-bound ( L~ f)) by EUCLID: 52;

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

      then i <= ( len f) by A3, XXREAL_0: 2;

      then

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

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

      then

       A9: ((f /. i) `2 ) >= ( S-bound ( L~ f)) by PSCOMP_1: 24;

      now

        per cases by A4, A9, A6, A7, Th20;

          suppose p = (f /. i);

          hence thesis by A8, PARTFUN2: 2;

        end;

          suppose p = (f /. (i + 1));

          hence thesis by A5, PARTFUN2: 2;

        end;

          suppose

           A10: (p `2 ) = ((f /. i) `2 ) & (p `2 ) = ((f /. (i + 1)) `2 );

          then (f /. (i + 1)) in ( S-most ( L~ f)) by A1, A5, A7, Th11, GOBOARD1: 1;

          then

           A11: ((f /. (i + 1)) `1 ) >= (p `1 ) by PSCOMP_1: 55;

          ((f /. i) `1 ) <= ((f /. (i + 1)) `1 ) or ((f /. (i + 1)) `1 ) <= ((f /. i) `1 );

          then

           A12: ((f /. i) `1 ) <= (p `1 ) or ((f /. (i + 1)) `1 ) <= (p `1 ) by A4, TOPREAL1: 3;

          (f /. i) in ( S-most ( L~ f)) by A1, A8, A7, A10, Th11, GOBOARD1: 1;

          then ((f /. i) `1 ) >= (p `1 ) by PSCOMP_1: 55;

          then (p `1 ) = ((f /. i) `1 ) or (p `1 ) = ((f /. (i + 1)) `1 ) by A11, A12, XXREAL_0: 1;

          then p = (f /. i) or p = (f /. (i + 1)) by A10, TOPREAL3: 6;

          hence thesis by A8, A5, PARTFUN2: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: SPRECT_2:42

    

     Th42: ( S-max ( L~ f)) in ( rng f)

    proof

      set p = ( S-max ( L~ f));

      

       A1: ( len f) >= 2 by NAT_D: 60;

      consider i be Nat such that

       A2: 1 <= i and

       A3: (i + 1) <= ( len f) and

       A4: p in ( LSeg ((f /. i),(f /. (i + 1)))) by SPPOL_2: 14, SPRECT_1: 12;

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

      then

       A5: (i + 1) in ( dom f) by A3, FINSEQ_3: 25;

      then (f /. (i + 1)) in ( L~ f) by A1, GOBOARD1: 1;

      then

       A6: ((f /. (i + 1)) `2 ) >= ( S-bound ( L~ f)) by PSCOMP_1: 24;

      

       A7: (p `2 ) = ( S-bound ( L~ f)) by EUCLID: 52;

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

      then i <= ( len f) by A3, XXREAL_0: 2;

      then

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

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

      then

       A9: ((f /. i) `2 ) >= ( S-bound ( L~ f)) by PSCOMP_1: 24;

      now

        per cases by A4, A9, A6, A7, Th20;

          suppose p = (f /. i);

          hence thesis by A8, PARTFUN2: 2;

        end;

          suppose p = (f /. (i + 1));

          hence thesis by A5, PARTFUN2: 2;

        end;

          suppose

           A10: (p `2 ) = ((f /. i) `2 ) & (p `2 ) = ((f /. (i + 1)) `2 );

          then (f /. (i + 1)) in ( S-most ( L~ f)) by A1, A5, A7, Th11, GOBOARD1: 1;

          then

           A11: ((f /. (i + 1)) `1 ) <= (p `1 ) by PSCOMP_1: 55;

          ((f /. i) `1 ) >= ((f /. (i + 1)) `1 ) or ((f /. (i + 1)) `1 ) >= ((f /. i) `1 );

          then

           A12: ((f /. i) `1 ) >= (p `1 ) or ((f /. (i + 1)) `1 ) >= (p `1 ) by A4, TOPREAL1: 3;

          (f /. i) in ( S-most ( L~ f)) by A1, A8, A7, A10, Th11, GOBOARD1: 1;

          then ((f /. i) `1 ) <= (p `1 ) by PSCOMP_1: 55;

          then (p `1 ) = ((f /. i) `1 ) or (p `1 ) = ((f /. (i + 1)) `1 ) by A11, A12, XXREAL_0: 1;

          then p = (f /. i) or p = (f /. (i + 1)) by A10, TOPREAL3: 6;

          hence thesis by A8, A5, PARTFUN2: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: SPRECT_2:43

    

     Th43: ( W-min ( L~ f)) in ( rng f)

    proof

      set p = ( W-min ( L~ f));

      

       A1: ( len f) >= 2 by NAT_D: 60;

      consider i be Nat such that

       A2: 1 <= i and

       A3: (i + 1) <= ( len f) and

       A4: p in ( LSeg ((f /. i),(f /. (i + 1)))) by SPPOL_2: 14, SPRECT_1: 13;

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

      then

       A5: (i + 1) in ( dom f) by A3, FINSEQ_3: 25;

      then (f /. (i + 1)) in ( L~ f) by A1, GOBOARD1: 1;

      then

       A6: ((f /. (i + 1)) `1 ) >= ( W-bound ( L~ f)) by PSCOMP_1: 24;

      

       A7: (p `1 ) = ( W-bound ( L~ f)) by EUCLID: 52;

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

      then i <= ( len f) by A3, XXREAL_0: 2;

      then

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

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

      then

       A9: ((f /. i) `1 ) >= ( W-bound ( L~ f)) by PSCOMP_1: 24;

      now

        per cases by A4, A9, A6, A7, Th19;

          suppose p = (f /. i);

          hence thesis by A8, PARTFUN2: 2;

        end;

          suppose p = (f /. (i + 1));

          hence thesis by A5, PARTFUN2: 2;

        end;

          suppose

           A10: (p `1 ) = ((f /. i) `1 ) & (p `1 ) = ((f /. (i + 1)) `1 );

          then (f /. (i + 1)) in ( W-most ( L~ f)) by A1, A5, A7, Th12, GOBOARD1: 1;

          then

           A11: ((f /. (i + 1)) `2 ) >= (p `2 ) by PSCOMP_1: 31;

          ((f /. i) `2 ) <= ((f /. (i + 1)) `2 ) or ((f /. (i + 1)) `2 ) <= ((f /. i) `2 );

          then

           A12: ((f /. i) `2 ) <= (p `2 ) or ((f /. (i + 1)) `2 ) <= (p `2 ) by A4, TOPREAL1: 4;

          (f /. i) in ( W-most ( L~ f)) by A1, A8, A7, A10, Th12, GOBOARD1: 1;

          then ((f /. i) `2 ) >= (p `2 ) by PSCOMP_1: 31;

          then (p `2 ) = ((f /. i) `2 ) or (p `2 ) = ((f /. (i + 1)) `2 ) by A11, A12, XXREAL_0: 1;

          then p = (f /. i) or p = (f /. (i + 1)) by A10, TOPREAL3: 6;

          hence thesis by A8, A5, PARTFUN2: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: SPRECT_2:44

    

     Th44: ( W-max ( L~ f)) in ( rng f)

    proof

      set p = ( W-max ( L~ f));

      

       A1: ( len f) >= 2 by NAT_D: 60;

      consider i be Nat such that

       A2: 1 <= i and

       A3: (i + 1) <= ( len f) and

       A4: p in ( LSeg ((f /. i),(f /. (i + 1)))) by SPPOL_2: 14, SPRECT_1: 13;

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

      then

       A5: (i + 1) in ( dom f) by A3, FINSEQ_3: 25;

      then (f /. (i + 1)) in ( L~ f) by A1, GOBOARD1: 1;

      then

       A6: ((f /. (i + 1)) `1 ) >= ( W-bound ( L~ f)) by PSCOMP_1: 24;

      

       A7: (p `1 ) = ( W-bound ( L~ f)) by EUCLID: 52;

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

      then i <= ( len f) by A3, XXREAL_0: 2;

      then

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

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

      then

       A9: ((f /. i) `1 ) >= ( W-bound ( L~ f)) by PSCOMP_1: 24;

      now

        per cases by A4, A9, A6, A7, Th19;

          suppose p = (f /. i);

          hence thesis by A8, PARTFUN2: 2;

        end;

          suppose p = (f /. (i + 1));

          hence thesis by A5, PARTFUN2: 2;

        end;

          suppose

           A10: (p `1 ) = ((f /. i) `1 ) & (p `1 ) = ((f /. (i + 1)) `1 );

          then (f /. (i + 1)) in ( W-most ( L~ f)) by A1, A5, A7, Th12, GOBOARD1: 1;

          then

           A11: ((f /. (i + 1)) `2 ) <= (p `2 ) by PSCOMP_1: 31;

          ((f /. i) `2 ) >= ((f /. (i + 1)) `2 ) or ((f /. (i + 1)) `2 ) >= ((f /. i) `2 );

          then

           A12: ((f /. i) `2 ) >= (p `2 ) or ((f /. (i + 1)) `2 ) >= (p `2 ) by A4, TOPREAL1: 4;

          (f /. i) in ( W-most ( L~ f)) by A1, A8, A7, A10, Th12, GOBOARD1: 1;

          then ((f /. i) `2 ) <= (p `2 ) by PSCOMP_1: 31;

          then (p `2 ) = ((f /. i) `2 ) or (p `2 ) = ((f /. (i + 1)) `2 ) by A11, A12, XXREAL_0: 1;

          then p = (f /. i) or p = (f /. (i + 1)) by A10, TOPREAL3: 6;

          hence thesis by A8, A5, PARTFUN2: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: SPRECT_2:45

    

     Th45: ( E-min ( L~ f)) in ( rng f)

    proof

      set p = ( E-min ( L~ f));

      

       A1: ( len f) >= 2 by NAT_D: 60;

      consider i be Nat such that

       A2: 1 <= i and

       A3: (i + 1) <= ( len f) and

       A4: p in ( LSeg ((f /. i),(f /. (i + 1)))) by SPPOL_2: 14, SPRECT_1: 14;

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

      then

       A5: (i + 1) in ( dom f) by A3, FINSEQ_3: 25;

      then (f /. (i + 1)) in ( L~ f) by A1, GOBOARD1: 1;

      then

       A6: ((f /. (i + 1)) `1 ) <= ( E-bound ( L~ f)) by PSCOMP_1: 24;

      

       A7: (p `1 ) = ( E-bound ( L~ f)) by EUCLID: 52;

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

      then i <= ( len f) by A3, XXREAL_0: 2;

      then

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

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

      then

       A9: ((f /. i) `1 ) <= ( E-bound ( L~ f)) by PSCOMP_1: 24;

      now

        per cases by A4, A9, A6, A7, Th17;

          suppose p = (f /. i);

          hence thesis by A8, PARTFUN2: 2;

        end;

          suppose p = (f /. (i + 1));

          hence thesis by A5, PARTFUN2: 2;

        end;

          suppose

           A10: (p `1 ) = ((f /. i) `1 ) & (p `1 ) = ((f /. (i + 1)) `1 );

          then (f /. (i + 1)) in ( E-most ( L~ f)) by A1, A5, A7, Th13, GOBOARD1: 1;

          then

           A11: ((f /. (i + 1)) `2 ) >= (p `2 ) by PSCOMP_1: 47;

          ((f /. i) `2 ) <= ((f /. (i + 1)) `2 ) or ((f /. (i + 1)) `2 ) <= ((f /. i) `2 );

          then

           A12: ((f /. i) `2 ) <= (p `2 ) or ((f /. (i + 1)) `2 ) <= (p `2 ) by A4, TOPREAL1: 4;

          (f /. i) in ( E-most ( L~ f)) by A1, A8, A7, A10, Th13, GOBOARD1: 1;

          then ((f /. i) `2 ) >= (p `2 ) by PSCOMP_1: 47;

          then (p `2 ) = ((f /. i) `2 ) or (p `2 ) = ((f /. (i + 1)) `2 ) by A11, A12, XXREAL_0: 1;

          then p = (f /. i) or p = (f /. (i + 1)) by A10, TOPREAL3: 6;

          hence thesis by A8, A5, PARTFUN2: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: SPRECT_2:46

    

     Th46: ( E-max ( L~ f)) in ( rng f)

    proof

      set p = ( E-max ( L~ f));

      

       A1: ( len f) >= 2 by NAT_D: 60;

      consider i be Nat such that

       A2: 1 <= i and

       A3: (i + 1) <= ( len f) and

       A4: p in ( LSeg ((f /. i),(f /. (i + 1)))) by SPPOL_2: 14, SPRECT_1: 14;

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

      then

       A5: (i + 1) in ( dom f) by A3, FINSEQ_3: 25;

      then (f /. (i + 1)) in ( L~ f) by A1, GOBOARD1: 1;

      then

       A6: ((f /. (i + 1)) `1 ) <= ( E-bound ( L~ f)) by PSCOMP_1: 24;

      

       A7: (p `1 ) = ( E-bound ( L~ f)) by EUCLID: 52;

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

      then i <= ( len f) by A3, XXREAL_0: 2;

      then

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

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

      then

       A9: ((f /. i) `1 ) <= ( E-bound ( L~ f)) by PSCOMP_1: 24;

      now

        per cases by A4, A9, A6, A7, Th17;

          suppose p = (f /. i);

          hence thesis by A8, PARTFUN2: 2;

        end;

          suppose p = (f /. (i + 1));

          hence thesis by A5, PARTFUN2: 2;

        end;

          suppose

           A10: (p `1 ) = ((f /. i) `1 ) & (p `1 ) = ((f /. (i + 1)) `1 );

          then (f /. (i + 1)) in ( E-most ( L~ f)) by A1, A5, A7, Th13, GOBOARD1: 1;

          then

           A11: ((f /. (i + 1)) `2 ) <= (p `2 ) by PSCOMP_1: 47;

          ((f /. i) `2 ) >= ((f /. (i + 1)) `2 ) or ((f /. (i + 1)) `2 ) >= ((f /. i) `2 );

          then

           A12: ((f /. i) `2 ) >= (p `2 ) or ((f /. (i + 1)) `2 ) >= (p `2 ) by A4, TOPREAL1: 4;

          (f /. i) in ( E-most ( L~ f)) by A1, A8, A7, A10, Th13, GOBOARD1: 1;

          then ((f /. i) `2 ) <= (p `2 ) by PSCOMP_1: 47;

          then (p `2 ) = ((f /. i) `2 ) or (p `2 ) = ((f /. (i + 1)) `2 ) by A11, A12, XXREAL_0: 1;

          then p = (f /. i) or p = (f /. (i + 1)) by A10, TOPREAL3: 6;

          hence thesis by A8, A5, PARTFUN2: 2;

        end;

      end;

      hence thesis;

    end;

    reserve f for non constant standard special_circular_sequence;

    theorem :: SPRECT_2:47

    

     Th47: 1 <= i & i <= j & j < m & m <= n & n <= ( len f) & (1 < i or n < ( len f)) implies ( L~ ( mid (f,i,j))) misses ( L~ ( mid (f,m,n)))

    proof

      assume that

       A1: 1 <= i & i <= j and

       A2: j < m and

       A3: m <= n and

       A4: n <= ( len f) and

       A5: 1 < i or n < ( len f);

      set A = { ( LSeg (f,k)) : i <= k & k < j }, B = { ( LSeg (f,l)) : m <= l & l < n };

      1 <= j by A1, XXREAL_0: 2;

      then 1 < m by A2, XXREAL_0: 2;

      then

       A6: ( L~ ( mid (f,m,n))) = ( union B) by A3, A4, Th14;

      

       A7: for x,y be set st x in A & y in B holds x misses y

      proof

        let x,y be set;

        assume x in A;

        then

        consider k such that

         A8: x = ( LSeg (f,k)) and

         A9: i <= k and

         A10: k < j;

        assume y in B;

        then

        consider l such that

         A11: y = ( LSeg (f,l)) and

         A12: m <= l and

         A13: l < n;

        

         A14: l < ( len f) by A4, A13, XXREAL_0: 2;

        (l + 1) <= n by A13, NAT_1: 13;

        then

         A15: k > 1 or (l + 1) < ( len f) by A5, A9, XXREAL_0: 2;

        (k + 1) <= j by A10, NAT_1: 13;

        then (k + 1) < m by A2, XXREAL_0: 2;

        then (k + 1) < l by A12, XXREAL_0: 2;

        hence thesis by A8, A11, A14, A15, GOBOARD5:def 4;

      end;

      m <= ( len f) by A3, A4, XXREAL_0: 2;

      then j < ( len f) by A2, XXREAL_0: 2;

      then ( L~ ( mid (f,i,j))) = ( union A) by A1, Th14;

      hence thesis by A6, A7, ZFMISC_1: 126;

    end;

    theorem :: SPRECT_2:48

    

     Th48: 1 <= i & i <= j & j < m & m <= n & n <= ( len f) & (1 < i or n < ( len f)) implies ( L~ ( mid (f,i,j))) misses ( L~ ( mid (f,n,m)))

    proof

      ( mid (f,n,m)) = ( Rev ( mid (f,m,n))) by JORDAN4: 18;

      then ( L~ ( mid (f,n,m))) = ( L~ ( mid (f,m,n))) by SPPOL_2: 22;

      hence thesis by Th47;

    end;

    theorem :: SPRECT_2:49

    

     Th49: 1 <= i & i <= j & j < m & m <= n & n <= ( len f) & (1 < i or n < ( len f)) implies ( L~ ( mid (f,j,i))) misses ( L~ ( mid (f,n,m)))

    proof

      ( mid (f,i,j)) = ( Rev ( mid (f,j,i))) by JORDAN4: 18;

      then ( L~ ( mid (f,i,j))) = ( L~ ( mid (f,j,i))) by SPPOL_2: 22;

      hence thesis by Th48;

    end;

    theorem :: SPRECT_2:50

    

     Th50: 1 <= i & i <= j & j < m & m <= n & n <= ( len f) & (1 < i or n < ( len f)) implies ( L~ ( mid (f,j,i))) misses ( L~ ( mid (f,m,n)))

    proof

      ( mid (f,i,j)) = ( Rev ( mid (f,j,i))) by JORDAN4: 18;

      then ( L~ ( mid (f,i,j))) = ( L~ ( mid (f,j,i))) by SPPOL_2: 22;

      hence thesis by Th47;

    end;

    theorem :: SPRECT_2:51

    

     Th51: (( N-min ( L~ f)) `1 ) < (( N-max ( L~ f)) `1 )

    proof

      set p = ( N-min ( L~ f)), i = (p .. f);

      

       A1: ( len f) > (3 + 1) by GOBOARD7: 34;

      

       A2: ( len f) >= (1 + 1) by GOBOARD7: 34, XXREAL_0: 2;

      

       A3: p in ( rng f) by Th39;

      then

       A4: i in ( dom f) by FINSEQ_4: 20;

      then

       A5: 1 <= i & i <= ( len f) by FINSEQ_3: 25;

      

       A6: p = (f . i) by A3, FINSEQ_4: 19

      .= (f /. i) by A4, PARTFUN1:def 6;

      

       A7: (p `2 ) = ( N-bound ( L~ f)) by EUCLID: 52;

      per cases by A5, XXREAL_0: 1;

        suppose

         A8: i = 1 or i = ( len f);

        then p = (f /. 1) by A6, FINSEQ_6:def 1;

        then

         A9: p in ( LSeg (f,1)) by A2, TOPREAL1: 21;

        

         A10: (1 + 1) in ( dom f) by A2, FINSEQ_3: 25;

        then

         A11: (f /. (1 + 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A12: (f /. (1 + 1)) in ( LSeg (f,1)) by A2, TOPREAL1: 21;

        

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

        then (( len f) -' 1) > 3 by A1, XREAL_1: 6;

        then

         A14: (( len f) -' 1) > 1 by XXREAL_0: 2;

        then

         A15: (f /. (( len f) -' 1)) in ( LSeg (f,(( len f) -' 1))) by A13, TOPREAL1: 21;

        (( len f) -' 1) <= ( len f) by A13, NAT_1: 11;

        then

         A16: (( len f) -' 1) in ( dom f) by A14, FINSEQ_3: 25;

        then

         A17: (f /. (( len f) -' 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A18: (f /. 1) = (f /. ( len f)) by FINSEQ_6:def 1;

        then

         A19: p in ( LSeg (f,(( len f) -' 1))) by A6, A8, A13, A14, TOPREAL1: 21;

        

         A20: 1 in ( dom f) by FINSEQ_5: 6;

        then

         A21: p <> (f /. (1 + 1)) by A6, A8, A18, A10, GOBOARD7: 29;

        

         A22: ( len f) in ( dom f) by FINSEQ_5: 6;

        then

         A23: p <> (f /. (( len f) -' 1)) by A6, A8, A18, A13, A16, GOBOARD7: 29;

        

         A24: not (( LSeg (f,(( len f) -' 1))) is vertical & ( LSeg (f,1)) is vertical)

        proof

          assume ( LSeg (f,(( len f) -' 1))) is vertical & ( LSeg (f,1)) is vertical;

          then

           A25: (p `1 ) = ((f /. (1 + 1)) `1 ) & (p `1 ) = ((f /. (( len f) -' 1)) `1 ) by A19, A9, A15, A12, SPPOL_1:def 3;

          

           A26: ((f /. (1 + 1)) `2 ) <= ((f /. (( len f) -' 1)) `2 ) or ((f /. (1 + 1)) `2 ) >= ((f /. (( len f) -' 1)) `2 );

          

           A27: (p `2 ) >= ((f /. (1 + 1)) `2 ) & (p `2 ) >= ((f /. (( len f) -' 1)) `2 ) by A7, A17, A11, PSCOMP_1: 24;

          ( LSeg (f,1)) = ( LSeg ((f /. 1),(f /. (1 + 1)))) & ( LSeg (f,(( len f) -' 1))) = ( LSeg ((f /. 1),(f /. (( len f) -' 1)))) by A2, A18, A13, A14, TOPREAL1:def 3;

          then (f /. (( len f) -' 1)) in ( LSeg (f,1)) or (f /. (1 + 1)) in ( LSeg (f,(( len f) -' 1))) by A6, A8, A18, A25, A27, A26, GOBOARD7: 7;

          then (f /. (( len f) -' 1)) in (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) or (f /. (1 + 1)) in (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) by A15, A12, XBOOLE_0:def 4;

          then

           A28: (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) <> {(f /. 1)} by A6, A8, A18, A23, A21, TARSKI:def 1;

          (f . 1) = (f /. 1) by A20, PARTFUN1:def 6;

          hence contradiction by A28, JORDAN4: 42;

        end;

        now

          per cases by A24, SPPOL_1: 19;

            suppose ( LSeg (f,(( len f) -' 1))) is horizontal;

            then

             A29: (p `2 ) = ((f /. (( len f) -' 1)) `2 ) by A19, A15, SPPOL_1:def 2;

            then

             A30: (f /. (( len f) -' 1)) in ( N-most ( L~ f)) by A2, A7, A16, Th10, GOBOARD1: 1;

            then

             A31: ((f /. (( len f) -' 1)) `1 ) >= (p `1 ) by PSCOMP_1: 39;

            ((f /. (( len f) -' 1)) `1 ) <> (p `1 ) by A6, A8, A22, A18, A13, A16, A29, GOBOARD7: 29, TOPREAL3: 6;

            then

             A32: ((f /. (( len f) -' 1)) `1 ) > (p `1 ) by A31, XXREAL_0: 1;

            ((f /. (( len f) -' 1)) `1 ) <= (( N-max ( L~ f)) `1 ) by A30, PSCOMP_1: 39;

            hence thesis by A32, XXREAL_0: 2;

          end;

            suppose ( LSeg (f,1)) is horizontal;

            then

             A33: (p `2 ) = ((f /. (1 + 1)) `2 ) by A9, A12, SPPOL_1:def 2;

            then

             A34: (f /. (1 + 1)) in ( N-most ( L~ f)) by A2, A7, A10, Th10, GOBOARD1: 1;

            then

             A35: ((f /. (1 + 1)) `1 ) >= (p `1 ) by PSCOMP_1: 39;

            ((f /. (1 + 1)) `1 ) <> (p `1 ) by A6, A8, A20, A18, A10, A33, GOBOARD7: 29, TOPREAL3: 6;

            then

             A36: ((f /. (1 + 1)) `1 ) > (p `1 ) by A35, XXREAL_0: 1;

            ((f /. (1 + 1)) `1 ) <= (( N-max ( L~ f)) `1 ) by A34, PSCOMP_1: 39;

            hence thesis by A36, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

        suppose that

         A37: 1 < i and

         A38: i < ( len f);

        

         A39: ((i -' 1) + 1) = i by A37, XREAL_1: 235;

        then

         A40: (i -' 1) >= 1 by A37, NAT_1: 13;

        then

         A41: (f /. (i -' 1)) in ( LSeg (f,(i -' 1))) by A38, A39, TOPREAL1: 21;

        (i -' 1) <= i by A39, NAT_1: 11;

        then (i -' 1) <= ( len f) by A38, XXREAL_0: 2;

        then

         A42: (i -' 1) in ( dom f) by A40, FINSEQ_3: 25;

        then

         A43: (f /. (i -' 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A44: (i + 1) <= ( len f) by A38, NAT_1: 13;

        then

         A45: (f /. (i + 1)) in ( LSeg (f,i)) by A37, TOPREAL1: 21;

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

        then

         A46: (i + 1) in ( dom f) by A44, FINSEQ_3: 25;

        then

         A47: (f /. (i + 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A48: p <> (f /. (i + 1)) by A3, A6, A46, FINSEQ_4: 20, GOBOARD7: 29;

        

         A49: p in ( LSeg (f,i)) by A6, A37, A44, TOPREAL1: 21;

        

         A50: p in ( LSeg (f,(i -' 1))) by A6, A38, A39, A40, TOPREAL1: 21;

        

         A51: p <> (f /. (i -' 1)) by A4, A6, A39, A42, GOBOARD7: 29;

        

         A52: not (( LSeg (f,(i -' 1))) is vertical & ( LSeg (f,i)) is vertical)

        proof

          assume ( LSeg (f,(i -' 1))) is vertical & ( LSeg (f,i)) is vertical;

          then

           A53: (p `1 ) = ((f /. (i + 1)) `1 ) & (p `1 ) = ((f /. (i -' 1)) `1 ) by A50, A49, A41, A45, SPPOL_1:def 3;

          

           A54: ((f /. (i + 1)) `2 ) <= ((f /. (i -' 1)) `2 ) or ((f /. (i + 1)) `2 ) >= ((f /. (i -' 1)) `2 );

          

           A55: (p `2 ) >= ((f /. (i + 1)) `2 ) & (p `2 ) >= ((f /. (i -' 1)) `2 ) by A7, A43, A47, PSCOMP_1: 24;

          ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) & ( LSeg (f,(i -' 1))) = ( LSeg ((f /. i),(f /. (i -' 1)))) by A37, A38, A39, A40, A44, TOPREAL1:def 3;

          then (f /. (i -' 1)) in ( LSeg (f,i)) or (f /. (i + 1)) in ( LSeg (f,(i -' 1))) by A6, A53, A55, A54, GOBOARD7: 7;

          then (f /. (i -' 1)) in (( LSeg (f,(i -' 1))) /\ ( LSeg (f,i))) or (f /. (i + 1)) in (( LSeg (f,(i -' 1))) /\ ( LSeg (f,i))) by A41, A45, XBOOLE_0:def 4;

          then (((i -' 1) + 1) + 1) = ((i -' 1) + (1 + 1)) & (( LSeg (f,(i -' 1))) /\ ( LSeg (f,i))) <> {(f /. i)} by A6, A51, A48, TARSKI:def 1;

          hence contradiction by A39, A40, A44, TOPREAL1:def 6;

        end;

        now

          per cases by A52, SPPOL_1: 19;

            suppose ( LSeg (f,(i -' 1))) is horizontal;

            then

             A56: (p `2 ) = ((f /. (i -' 1)) `2 ) by A50, A41, SPPOL_1:def 2;

            then

             A57: (f /. (i -' 1)) in ( N-most ( L~ f)) by A2, A7, A42, Th10, GOBOARD1: 1;

            then

             A58: ((f /. (i -' 1)) `1 ) >= (p `1 ) by PSCOMP_1: 39;

            ((f /. (i -' 1)) `1 ) <> (p `1 ) by A4, A6, A39, A42, A56, GOBOARD7: 29, TOPREAL3: 6;

            then

             A59: ((f /. (i -' 1)) `1 ) > (p `1 ) by A58, XXREAL_0: 1;

            ((f /. (i -' 1)) `1 ) <= (( N-max ( L~ f)) `1 ) by A57, PSCOMP_1: 39;

            hence thesis by A59, XXREAL_0: 2;

          end;

            suppose ( LSeg (f,i)) is horizontal;

            then

             A60: (p `2 ) = ((f /. (i + 1)) `2 ) by A49, A45, SPPOL_1:def 2;

            then

             A61: (f /. (i + 1)) in ( N-most ( L~ f)) by A2, A7, A46, Th10, GOBOARD1: 1;

            then

             A62: ((f /. (i + 1)) `1 ) >= (p `1 ) by PSCOMP_1: 39;

            ((f /. (i + 1)) `1 ) <> (p `1 ) by A4, A6, A46, A60, GOBOARD7: 29, TOPREAL3: 6;

            then

             A63: ((f /. (i + 1)) `1 ) > (p `1 ) by A62, XXREAL_0: 1;

            ((f /. (i + 1)) `1 ) <= (( N-max ( L~ f)) `1 ) by A61, PSCOMP_1: 39;

            hence thesis by A63, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: SPRECT_2:52

    

     Th52: ( N-min ( L~ f)) <> ( N-max ( L~ f))

    proof

      (( N-min ( L~ f)) `1 ) < (( N-max ( L~ f)) `1 ) by Th51;

      hence thesis;

    end;

    theorem :: SPRECT_2:53

    

     Th53: (( E-min ( L~ f)) `2 ) < (( E-max ( L~ f)) `2 )

    proof

      set p = ( E-min ( L~ f)), i = (p .. f);

      

       A1: ( len f) > (3 + 1) by GOBOARD7: 34;

      

       A2: ( len f) >= (1 + 1) by GOBOARD7: 34, XXREAL_0: 2;

      

       A3: p in ( rng f) by Th45;

      then

       A4: i in ( dom f) by FINSEQ_4: 20;

      then

       A5: 1 <= i & i <= ( len f) by FINSEQ_3: 25;

      

       A6: p = (f . i) by A3, FINSEQ_4: 19

      .= (f /. i) by A4, PARTFUN1:def 6;

      

       A7: (p `1 ) = ( E-bound ( L~ f)) by EUCLID: 52;

      per cases by A5, XXREAL_0: 1;

        suppose

         A8: i = 1 or i = ( len f);

        then p = (f /. 1) by A6, FINSEQ_6:def 1;

        then

         A9: p in ( LSeg (f,1)) by A2, TOPREAL1: 21;

        

         A10: (1 + 1) in ( dom f) by A2, FINSEQ_3: 25;

        then

         A11: (f /. (1 + 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A12: (f /. (1 + 1)) in ( LSeg (f,1)) by A2, TOPREAL1: 21;

        

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

        then (( len f) -' 1) > 3 by A1, XREAL_1: 6;

        then

         A14: (( len f) -' 1) > 1 by XXREAL_0: 2;

        then

         A15: (f /. (( len f) -' 1)) in ( LSeg (f,(( len f) -' 1))) by A13, TOPREAL1: 21;

        (( len f) -' 1) <= ( len f) by A13, NAT_1: 11;

        then

         A16: (( len f) -' 1) in ( dom f) by A14, FINSEQ_3: 25;

        then

         A17: (f /. (( len f) -' 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A18: (f /. 1) = (f /. ( len f)) by FINSEQ_6:def 1;

        then

         A19: p in ( LSeg (f,(( len f) -' 1))) by A6, A8, A13, A14, TOPREAL1: 21;

        

         A20: 1 in ( dom f) by FINSEQ_5: 6;

        then

         A21: p <> (f /. (1 + 1)) by A6, A8, A18, A10, GOBOARD7: 29;

        

         A22: ( len f) in ( dom f) by FINSEQ_5: 6;

        then

         A23: p <> (f /. (( len f) -' 1)) by A6, A8, A18, A13, A16, GOBOARD7: 29;

        

         A24: not (( LSeg (f,(( len f) -' 1))) is horizontal & ( LSeg (f,1)) is horizontal)

        proof

          assume ( LSeg (f,(( len f) -' 1))) is horizontal & ( LSeg (f,1)) is horizontal;

          then

           A25: (p `2 ) = ((f /. (1 + 1)) `2 ) & (p `2 ) = ((f /. (( len f) -' 1)) `2 ) by A19, A9, A15, A12, SPPOL_1:def 2;

          

           A26: ((f /. (1 + 1)) `1 ) <= ((f /. (( len f) -' 1)) `1 ) or ((f /. (1 + 1)) `1 ) >= ((f /. (( len f) -' 1)) `1 );

          

           A27: (p `1 ) >= ((f /. (1 + 1)) `1 ) & (p `1 ) >= ((f /. (( len f) -' 1)) `1 ) by A7, A17, A11, PSCOMP_1: 24;

          ( LSeg (f,1)) = ( LSeg ((f /. 1),(f /. (1 + 1)))) & ( LSeg (f,(( len f) -' 1))) = ( LSeg ((f /. 1),(f /. (( len f) -' 1)))) by A2, A18, A13, A14, TOPREAL1:def 3;

          then (f /. (( len f) -' 1)) in ( LSeg (f,1)) or (f /. (1 + 1)) in ( LSeg (f,(( len f) -' 1))) by A6, A8, A18, A25, A27, A26, GOBOARD7: 8;

          then (f /. (( len f) -' 1)) in (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) or (f /. (1 + 1)) in (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) by A15, A12, XBOOLE_0:def 4;

          then

           A28: (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) <> {(f /. 1)} by A6, A8, A18, A23, A21, TARSKI:def 1;

          (f . 1) = (f /. 1) by A20, PARTFUN1:def 6;

          hence contradiction by A28, JORDAN4: 42;

        end;

        now

          per cases by A24, SPPOL_1: 19;

            suppose ( LSeg (f,(( len f) -' 1))) is vertical;

            then

             A29: (p `1 ) = ((f /. (( len f) -' 1)) `1 ) by A19, A15, SPPOL_1:def 3;

            then

             A30: (f /. (( len f) -' 1)) in ( E-most ( L~ f)) by A2, A7, A16, Th13, GOBOARD1: 1;

            then

             A31: ((f /. (( len f) -' 1)) `2 ) >= (p `2 ) by PSCOMP_1: 47;

            ((f /. (( len f) -' 1)) `2 ) <> (p `2 ) by A6, A8, A22, A18, A13, A16, A29, GOBOARD7: 29, TOPREAL3: 6;

            then

             A32: ((f /. (( len f) -' 1)) `2 ) > (p `2 ) by A31, XXREAL_0: 1;

            ((f /. (( len f) -' 1)) `2 ) <= (( E-max ( L~ f)) `2 ) by A30, PSCOMP_1: 47;

            hence thesis by A32, XXREAL_0: 2;

          end;

            suppose ( LSeg (f,1)) is vertical;

            then

             A33: (p `1 ) = ((f /. (1 + 1)) `1 ) by A9, A12, SPPOL_1:def 3;

            then

             A34: (f /. (1 + 1)) in ( E-most ( L~ f)) by A2, A7, A10, Th13, GOBOARD1: 1;

            then

             A35: ((f /. (1 + 1)) `2 ) >= (p `2 ) by PSCOMP_1: 47;

            ((f /. (1 + 1)) `2 ) <> (p `2 ) by A6, A8, A20, A18, A10, A33, GOBOARD7: 29, TOPREAL3: 6;

            then

             A36: ((f /. (1 + 1)) `2 ) > (p `2 ) by A35, XXREAL_0: 1;

            ((f /. (1 + 1)) `2 ) <= (( E-max ( L~ f)) `2 ) by A34, PSCOMP_1: 47;

            hence thesis by A36, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

        suppose that

         A37: 1 < i and

         A38: i < ( len f);

        

         A39: ((i -' 1) + 1) = i by A37, XREAL_1: 235;

        then

         A40: (i -' 1) >= 1 by A37, NAT_1: 13;

        then

         A41: (f /. (i -' 1)) in ( LSeg (f,(i -' 1))) by A38, A39, TOPREAL1: 21;

        (i -' 1) <= i by A39, NAT_1: 11;

        then (i -' 1) <= ( len f) by A38, XXREAL_0: 2;

        then

         A42: (i -' 1) in ( dom f) by A40, FINSEQ_3: 25;

        then

         A43: (f /. (i -' 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A44: (i + 1) <= ( len f) by A38, NAT_1: 13;

        then

         A45: (f /. (i + 1)) in ( LSeg (f,i)) by A37, TOPREAL1: 21;

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

        then

         A46: (i + 1) in ( dom f) by A44, FINSEQ_3: 25;

        then

         A47: (f /. (i + 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A48: p <> (f /. (i + 1)) by A3, A6, A46, FINSEQ_4: 20, GOBOARD7: 29;

        

         A49: p in ( LSeg (f,i)) by A6, A37, A44, TOPREAL1: 21;

        

         A50: p in ( LSeg (f,(i -' 1))) by A6, A38, A39, A40, TOPREAL1: 21;

        

         A51: p <> (f /. (i -' 1)) by A4, A6, A39, A42, GOBOARD7: 29;

        

         A52: not (( LSeg (f,(i -' 1))) is horizontal & ( LSeg (f,i)) is horizontal)

        proof

          assume ( LSeg (f,(i -' 1))) is horizontal & ( LSeg (f,i)) is horizontal;

          then

           A53: (p `2 ) = ((f /. (i + 1)) `2 ) & (p `2 ) = ((f /. (i -' 1)) `2 ) by A50, A49, A41, A45, SPPOL_1:def 2;

          

           A54: ((f /. (i + 1)) `1 ) <= ((f /. (i -' 1)) `1 ) or ((f /. (i + 1)) `1 ) >= ((f /. (i -' 1)) `1 );

          

           A55: (p `1 ) >= ((f /. (i + 1)) `1 ) & (p `1 ) >= ((f /. (i -' 1)) `1 ) by A7, A43, A47, PSCOMP_1: 24;

          ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) & ( LSeg (f,(i -' 1))) = ( LSeg ((f /. i),(f /. (i -' 1)))) by A37, A38, A39, A40, A44, TOPREAL1:def 3;

          then (f /. (i -' 1)) in ( LSeg (f,i)) or (f /. (i + 1)) in ( LSeg (f,(i -' 1))) by A6, A53, A55, A54, GOBOARD7: 8;

          then (f /. (i -' 1)) in (( LSeg (f,(i -' 1))) /\ ( LSeg (f,i))) or (f /. (i + 1)) in (( LSeg (f,(i -' 1))) /\ ( LSeg (f,i))) by A41, A45, XBOOLE_0:def 4;

          then (((i -' 1) + 1) + 1) = ((i -' 1) + (1 + 1)) & (( LSeg (f,(i -' 1))) /\ ( LSeg (f,i))) <> {(f /. i)} by A6, A51, A48, TARSKI:def 1;

          hence contradiction by A39, A40, A44, TOPREAL1:def 6;

        end;

        now

          per cases by A52, SPPOL_1: 19;

            suppose ( LSeg (f,(i -' 1))) is vertical;

            then

             A56: (p `1 ) = ((f /. (i -' 1)) `1 ) by A50, A41, SPPOL_1:def 3;

            then

             A57: (f /. (i -' 1)) in ( E-most ( L~ f)) by A2, A7, A42, Th13, GOBOARD1: 1;

            then

             A58: ((f /. (i -' 1)) `2 ) >= (p `2 ) by PSCOMP_1: 47;

            ((f /. (i -' 1)) `2 ) <> (p `2 ) by A4, A6, A39, A42, A56, GOBOARD7: 29, TOPREAL3: 6;

            then

             A59: ((f /. (i -' 1)) `2 ) > (p `2 ) by A58, XXREAL_0: 1;

            ((f /. (i -' 1)) `2 ) <= (( E-max ( L~ f)) `2 ) by A57, PSCOMP_1: 47;

            hence thesis by A59, XXREAL_0: 2;

          end;

            suppose ( LSeg (f,i)) is vertical;

            then

             A60: (p `1 ) = ((f /. (i + 1)) `1 ) by A49, A45, SPPOL_1:def 3;

            then

             A61: (f /. (i + 1)) in ( E-most ( L~ f)) by A2, A7, A46, Th13, GOBOARD1: 1;

            then

             A62: ((f /. (i + 1)) `2 ) >= (p `2 ) by PSCOMP_1: 47;

            ((f /. (i + 1)) `2 ) <> (p `2 ) by A4, A6, A46, A60, GOBOARD7: 29, TOPREAL3: 6;

            then

             A63: ((f /. (i + 1)) `2 ) > (p `2 ) by A62, XXREAL_0: 1;

            ((f /. (i + 1)) `2 ) <= (( E-max ( L~ f)) `2 ) by A61, PSCOMP_1: 47;

            hence thesis by A63, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: SPRECT_2:54

    ( E-min ( L~ f)) <> ( E-max ( L~ f))

    proof

      (( E-min ( L~ f)) `2 ) < (( E-max ( L~ f)) `2 ) by Th53;

      hence thesis;

    end;

    theorem :: SPRECT_2:55

    

     Th55: (( S-min ( L~ f)) `1 ) < (( S-max ( L~ f)) `1 )

    proof

      set p = ( S-min ( L~ f)), i = (p .. f);

      

       A1: ( len f) > (3 + 1) by GOBOARD7: 34;

      

       A2: ( len f) >= (1 + 1) by GOBOARD7: 34, XXREAL_0: 2;

      

       A3: p in ( rng f) by Th41;

      then

       A4: i in ( dom f) by FINSEQ_4: 20;

      then

       A5: 1 <= i & i <= ( len f) by FINSEQ_3: 25;

      

       A6: p = (f . i) by A3, FINSEQ_4: 19

      .= (f /. i) by A4, PARTFUN1:def 6;

      

       A7: (p `2 ) = ( S-bound ( L~ f)) by EUCLID: 52;

      per cases by A5, XXREAL_0: 1;

        suppose

         A8: i = 1 or i = ( len f);

        then p = (f /. 1) by A6, FINSEQ_6:def 1;

        then

         A9: p in ( LSeg (f,1)) by A2, TOPREAL1: 21;

        

         A10: (1 + 1) in ( dom f) by A2, FINSEQ_3: 25;

        then

         A11: (f /. (1 + 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A12: (f /. (1 + 1)) in ( LSeg (f,1)) by A2, TOPREAL1: 21;

        

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

        then (( len f) -' 1) > 3 by A1, XREAL_1: 6;

        then

         A14: (( len f) -' 1) > 1 by XXREAL_0: 2;

        then

         A15: (f /. (( len f) -' 1)) in ( LSeg (f,(( len f) -' 1))) by A13, TOPREAL1: 21;

        (( len f) -' 1) <= ( len f) by A13, NAT_1: 11;

        then

         A16: (( len f) -' 1) in ( dom f) by A14, FINSEQ_3: 25;

        then

         A17: (f /. (( len f) -' 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A18: (f /. 1) = (f /. ( len f)) by FINSEQ_6:def 1;

        then

         A19: p in ( LSeg (f,(( len f) -' 1))) by A6, A8, A13, A14, TOPREAL1: 21;

        

         A20: 1 in ( dom f) by FINSEQ_5: 6;

        then

         A21: p <> (f /. (1 + 1)) by A6, A8, A18, A10, GOBOARD7: 29;

        

         A22: ( len f) in ( dom f) by FINSEQ_5: 6;

        then

         A23: p <> (f /. (( len f) -' 1)) by A6, A8, A18, A13, A16, GOBOARD7: 29;

        

         A24: not (( LSeg (f,(( len f) -' 1))) is vertical & ( LSeg (f,1)) is vertical)

        proof

          assume ( LSeg (f,(( len f) -' 1))) is vertical & ( LSeg (f,1)) is vertical;

          then

           A25: (p `1 ) = ((f /. (1 + 1)) `1 ) & (p `1 ) = ((f /. (( len f) -' 1)) `1 ) by A19, A9, A15, A12, SPPOL_1:def 3;

          

           A26: ((f /. (1 + 1)) `2 ) <= ((f /. (( len f) -' 1)) `2 ) or ((f /. (1 + 1)) `2 ) >= ((f /. (( len f) -' 1)) `2 );

          

           A27: (p `2 ) <= ((f /. (1 + 1)) `2 ) & (p `2 ) <= ((f /. (( len f) -' 1)) `2 ) by A7, A17, A11, PSCOMP_1: 24;

          ( LSeg (f,1)) = ( LSeg ((f /. 1),(f /. (1 + 1)))) & ( LSeg (f,(( len f) -' 1))) = ( LSeg ((f /. 1),(f /. (( len f) -' 1)))) by A2, A18, A13, A14, TOPREAL1:def 3;

          then (f /. (( len f) -' 1)) in ( LSeg (f,1)) or (f /. (1 + 1)) in ( LSeg (f,(( len f) -' 1))) by A6, A8, A18, A25, A27, A26, GOBOARD7: 7;

          then (f /. (( len f) -' 1)) in (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) or (f /. (1 + 1)) in (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) by A15, A12, XBOOLE_0:def 4;

          then

           A28: (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) <> {(f /. 1)} by A6, A8, A18, A23, A21, TARSKI:def 1;

          (f . 1) = (f /. 1) by A20, PARTFUN1:def 6;

          hence contradiction by A28, JORDAN4: 42;

        end;

        now

          per cases by A24, SPPOL_1: 19;

            suppose ( LSeg (f,(( len f) -' 1))) is horizontal;

            then

             A29: (p `2 ) = ((f /. (( len f) -' 1)) `2 ) by A19, A15, SPPOL_1:def 2;

            then

             A30: (f /. (( len f) -' 1)) in ( S-most ( L~ f)) by A2, A7, A16, Th11, GOBOARD1: 1;

            then

             A31: ((f /. (( len f) -' 1)) `1 ) >= (p `1 ) by PSCOMP_1: 55;

            ((f /. (( len f) -' 1)) `1 ) <> (p `1 ) by A6, A8, A22, A18, A13, A16, A29, GOBOARD7: 29, TOPREAL3: 6;

            then

             A32: ((f /. (( len f) -' 1)) `1 ) > (p `1 ) by A31, XXREAL_0: 1;

            ((f /. (( len f) -' 1)) `1 ) <= (( S-max ( L~ f)) `1 ) by A30, PSCOMP_1: 55;

            hence thesis by A32, XXREAL_0: 2;

          end;

            suppose ( LSeg (f,1)) is horizontal;

            then

             A33: (p `2 ) = ((f /. (1 + 1)) `2 ) by A9, A12, SPPOL_1:def 2;

            then

             A34: (f /. (1 + 1)) in ( S-most ( L~ f)) by A2, A7, A10, Th11, GOBOARD1: 1;

            then

             A35: ((f /. (1 + 1)) `1 ) >= (p `1 ) by PSCOMP_1: 55;

            ((f /. (1 + 1)) `1 ) <> (p `1 ) by A6, A8, A20, A18, A10, A33, GOBOARD7: 29, TOPREAL3: 6;

            then

             A36: ((f /. (1 + 1)) `1 ) > (p `1 ) by A35, XXREAL_0: 1;

            ((f /. (1 + 1)) `1 ) <= (( S-max ( L~ f)) `1 ) by A34, PSCOMP_1: 55;

            hence thesis by A36, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

        suppose that

         A37: 1 < i and

         A38: i < ( len f);

        

         A39: ((i -' 1) + 1) = i by A37, XREAL_1: 235;

        then

         A40: (i -' 1) >= 1 by A37, NAT_1: 13;

        then

         A41: (f /. (i -' 1)) in ( LSeg (f,(i -' 1))) by A38, A39, TOPREAL1: 21;

        (i -' 1) <= i by A39, NAT_1: 11;

        then (i -' 1) <= ( len f) by A38, XXREAL_0: 2;

        then

         A42: (i -' 1) in ( dom f) by A40, FINSEQ_3: 25;

        then

         A43: (f /. (i -' 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A44: (i + 1) <= ( len f) by A38, NAT_1: 13;

        then

         A45: (f /. (i + 1)) in ( LSeg (f,i)) by A37, TOPREAL1: 21;

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

        then

         A46: (i + 1) in ( dom f) by A44, FINSEQ_3: 25;

        then

         A47: (f /. (i + 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A48: p <> (f /. (i + 1)) by A3, A6, A46, FINSEQ_4: 20, GOBOARD7: 29;

        

         A49: p in ( LSeg (f,i)) by A6, A37, A44, TOPREAL1: 21;

        

         A50: p in ( LSeg (f,(i -' 1))) by A6, A38, A39, A40, TOPREAL1: 21;

        

         A51: p <> (f /. (i -' 1)) by A4, A6, A39, A42, GOBOARD7: 29;

        

         A52: not (( LSeg (f,(i -' 1))) is vertical & ( LSeg (f,i)) is vertical)

        proof

          assume ( LSeg (f,(i -' 1))) is vertical & ( LSeg (f,i)) is vertical;

          then

           A53: (p `1 ) = ((f /. (i + 1)) `1 ) & (p `1 ) = ((f /. (i -' 1)) `1 ) by A50, A49, A41, A45, SPPOL_1:def 3;

          

           A54: ((f /. (i + 1)) `2 ) <= ((f /. (i -' 1)) `2 ) or ((f /. (i + 1)) `2 ) >= ((f /. (i -' 1)) `2 );

          

           A55: (p `2 ) <= ((f /. (i + 1)) `2 ) & (p `2 ) <= ((f /. (i -' 1)) `2 ) by A7, A43, A47, PSCOMP_1: 24;

          ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) & ( LSeg (f,(i -' 1))) = ( LSeg ((f /. i),(f /. (i -' 1)))) by A37, A38, A39, A40, A44, TOPREAL1:def 3;

          then (f /. (i -' 1)) in ( LSeg (f,i)) or (f /. (i + 1)) in ( LSeg (f,(i -' 1))) by A6, A53, A55, A54, GOBOARD7: 7;

          then (f /. (i -' 1)) in (( LSeg (f,(i -' 1))) /\ ( LSeg (f,i))) or (f /. (i + 1)) in (( LSeg (f,(i -' 1))) /\ ( LSeg (f,i))) by A41, A45, XBOOLE_0:def 4;

          then (((i -' 1) + 1) + 1) = ((i -' 1) + (1 + 1)) & (( LSeg (f,(i -' 1))) /\ ( LSeg (f,i))) <> {(f /. i)} by A6, A51, A48, TARSKI:def 1;

          hence contradiction by A39, A40, A44, TOPREAL1:def 6;

        end;

        now

          per cases by A52, SPPOL_1: 19;

            suppose ( LSeg (f,(i -' 1))) is horizontal;

            then

             A56: (p `2 ) = ((f /. (i -' 1)) `2 ) by A50, A41, SPPOL_1:def 2;

            then

             A57: (f /. (i -' 1)) in ( S-most ( L~ f)) by A2, A7, A42, Th11, GOBOARD1: 1;

            then

             A58: ((f /. (i -' 1)) `1 ) >= (p `1 ) by PSCOMP_1: 55;

            ((f /. (i -' 1)) `1 ) <> (p `1 ) by A4, A6, A39, A42, A56, GOBOARD7: 29, TOPREAL3: 6;

            then

             A59: ((f /. (i -' 1)) `1 ) > (p `1 ) by A58, XXREAL_0: 1;

            ((f /. (i -' 1)) `1 ) <= (( S-max ( L~ f)) `1 ) by A57, PSCOMP_1: 55;

            hence thesis by A59, XXREAL_0: 2;

          end;

            suppose ( LSeg (f,i)) is horizontal;

            then

             A60: (p `2 ) = ((f /. (i + 1)) `2 ) by A49, A45, SPPOL_1:def 2;

            then

             A61: (f /. (i + 1)) in ( S-most ( L~ f)) by A2, A7, A46, Th11, GOBOARD1: 1;

            then

             A62: ((f /. (i + 1)) `1 ) >= (p `1 ) by PSCOMP_1: 55;

            ((f /. (i + 1)) `1 ) <> (p `1 ) by A4, A6, A46, A60, GOBOARD7: 29, TOPREAL3: 6;

            then

             A63: ((f /. (i + 1)) `1 ) > (p `1 ) by A62, XXREAL_0: 1;

            ((f /. (i + 1)) `1 ) <= (( S-max ( L~ f)) `1 ) by A61, PSCOMP_1: 55;

            hence thesis by A63, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: SPRECT_2:56

    

     Th56: ( S-min ( L~ f)) <> ( S-max ( L~ f))

    proof

      (( S-min ( L~ f)) `1 ) < (( S-max ( L~ f)) `1 ) by Th55;

      hence thesis;

    end;

    theorem :: SPRECT_2:57

    

     Th57: (( W-min ( L~ f)) `2 ) < (( W-max ( L~ f)) `2 )

    proof

      set p = ( W-min ( L~ f)), i = (p .. f);

      

       A1: ( len f) > (3 + 1) by GOBOARD7: 34;

      

       A2: ( len f) >= (1 + 1) by GOBOARD7: 34, XXREAL_0: 2;

      

       A3: p in ( rng f) by Th43;

      then

       A4: i in ( dom f) by FINSEQ_4: 20;

      then

       A5: 1 <= i & i <= ( len f) by FINSEQ_3: 25;

      

       A6: p = (f . i) by A3, FINSEQ_4: 19

      .= (f /. i) by A4, PARTFUN1:def 6;

      

       A7: (p `1 ) = ( W-bound ( L~ f)) by EUCLID: 52;

      per cases by A5, XXREAL_0: 1;

        suppose

         A8: i = 1 or i = ( len f);

        then p = (f /. 1) by A6, FINSEQ_6:def 1;

        then

         A9: p in ( LSeg (f,1)) by A2, TOPREAL1: 21;

        

         A10: (1 + 1) in ( dom f) by A2, FINSEQ_3: 25;

        then

         A11: (f /. (1 + 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A12: (f /. (1 + 1)) in ( LSeg (f,1)) by A2, TOPREAL1: 21;

        

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

        then (( len f) -' 1) > 3 by A1, XREAL_1: 6;

        then

         A14: (( len f) -' 1) > 1 by XXREAL_0: 2;

        then

         A15: (f /. (( len f) -' 1)) in ( LSeg (f,(( len f) -' 1))) by A13, TOPREAL1: 21;

        (( len f) -' 1) <= ( len f) by A13, NAT_1: 11;

        then

         A16: (( len f) -' 1) in ( dom f) by A14, FINSEQ_3: 25;

        then

         A17: (f /. (( len f) -' 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A18: (f /. 1) = (f /. ( len f)) by FINSEQ_6:def 1;

        then

         A19: p in ( LSeg (f,(( len f) -' 1))) by A6, A8, A13, A14, TOPREAL1: 21;

        

         A20: 1 in ( dom f) by FINSEQ_5: 6;

        then

         A21: p <> (f /. (1 + 1)) by A6, A8, A18, A10, GOBOARD7: 29;

        

         A22: ( len f) in ( dom f) by FINSEQ_5: 6;

        then

         A23: p <> (f /. (( len f) -' 1)) by A6, A8, A18, A13, A16, GOBOARD7: 29;

        

         A24: not (( LSeg (f,(( len f) -' 1))) is horizontal & ( LSeg (f,1)) is horizontal)

        proof

          assume ( LSeg (f,(( len f) -' 1))) is horizontal & ( LSeg (f,1)) is horizontal;

          then

           A25: (p `2 ) = ((f /. (1 + 1)) `2 ) & (p `2 ) = ((f /. (( len f) -' 1)) `2 ) by A19, A9, A15, A12, SPPOL_1:def 2;

          

           A26: ((f /. (1 + 1)) `1 ) <= ((f /. (( len f) -' 1)) `1 ) or ((f /. (1 + 1)) `1 ) >= ((f /. (( len f) -' 1)) `1 );

          

           A27: (p `1 ) <= ((f /. (1 + 1)) `1 ) & (p `1 ) <= ((f /. (( len f) -' 1)) `1 ) by A7, A17, A11, PSCOMP_1: 24;

          ( LSeg (f,1)) = ( LSeg ((f /. 1),(f /. (1 + 1)))) & ( LSeg (f,(( len f) -' 1))) = ( LSeg ((f /. 1),(f /. (( len f) -' 1)))) by A2, A18, A13, A14, TOPREAL1:def 3;

          then (f /. (( len f) -' 1)) in ( LSeg (f,1)) or (f /. (1 + 1)) in ( LSeg (f,(( len f) -' 1))) by A6, A8, A18, A25, A27, A26, GOBOARD7: 8;

          then (f /. (( len f) -' 1)) in (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) or (f /. (1 + 1)) in (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) by A15, A12, XBOOLE_0:def 4;

          then

           A28: (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,1))) <> {(f /. 1)} by A6, A8, A18, A23, A21, TARSKI:def 1;

          (f . 1) = (f /. 1) by A20, PARTFUN1:def 6;

          hence contradiction by A28, JORDAN4: 42;

        end;

        now

          per cases by A24, SPPOL_1: 19;

            suppose ( LSeg (f,(( len f) -' 1))) is vertical;

            then

             A29: (p `1 ) = ((f /. (( len f) -' 1)) `1 ) by A19, A15, SPPOL_1:def 3;

            then

             A30: (f /. (( len f) -' 1)) in ( W-most ( L~ f)) by A2, A7, A16, Th12, GOBOARD1: 1;

            then

             A31: ((f /. (( len f) -' 1)) `2 ) >= (p `2 ) by PSCOMP_1: 31;

            ((f /. (( len f) -' 1)) `2 ) <> (p `2 ) by A6, A8, A22, A18, A13, A16, A29, GOBOARD7: 29, TOPREAL3: 6;

            then

             A32: ((f /. (( len f) -' 1)) `2 ) > (p `2 ) by A31, XXREAL_0: 1;

            ((f /. (( len f) -' 1)) `2 ) <= (( W-max ( L~ f)) `2 ) by A30, PSCOMP_1: 31;

            hence thesis by A32, XXREAL_0: 2;

          end;

            suppose ( LSeg (f,1)) is vertical;

            then

             A33: (p `1 ) = ((f /. (1 + 1)) `1 ) by A9, A12, SPPOL_1:def 3;

            then

             A34: (f /. (1 + 1)) in ( W-most ( L~ f)) by A2, A7, A10, Th12, GOBOARD1: 1;

            then

             A35: ((f /. (1 + 1)) `2 ) >= (p `2 ) by PSCOMP_1: 31;

            ((f /. (1 + 1)) `2 ) <> (p `2 ) by A6, A8, A20, A18, A10, A33, GOBOARD7: 29, TOPREAL3: 6;

            then

             A36: ((f /. (1 + 1)) `2 ) > (p `2 ) by A35, XXREAL_0: 1;

            ((f /. (1 + 1)) `2 ) <= (( W-max ( L~ f)) `2 ) by A34, PSCOMP_1: 31;

            hence thesis by A36, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

        suppose that

         A37: 1 < i and

         A38: i < ( len f);

        

         A39: ((i -' 1) + 1) = i by A37, XREAL_1: 235;

        then

         A40: (i -' 1) >= 1 by A37, NAT_1: 13;

        then

         A41: (f /. (i -' 1)) in ( LSeg (f,(i -' 1))) by A38, A39, TOPREAL1: 21;

        (i -' 1) <= i by A39, NAT_1: 11;

        then (i -' 1) <= ( len f) by A38, XXREAL_0: 2;

        then

         A42: (i -' 1) in ( dom f) by A40, FINSEQ_3: 25;

        then

         A43: (f /. (i -' 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A44: (i + 1) <= ( len f) by A38, NAT_1: 13;

        then

         A45: (f /. (i + 1)) in ( LSeg (f,i)) by A37, TOPREAL1: 21;

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

        then

         A46: (i + 1) in ( dom f) by A44, FINSEQ_3: 25;

        then

         A47: (f /. (i + 1)) in ( L~ f) by A1, GOBOARD1: 1, XXREAL_0: 2;

        

         A48: p <> (f /. (i + 1)) by A3, A6, A46, FINSEQ_4: 20, GOBOARD7: 29;

        

         A49: p in ( LSeg (f,i)) by A6, A37, A44, TOPREAL1: 21;

        

         A50: p in ( LSeg (f,(i -' 1))) by A6, A38, A39, A40, TOPREAL1: 21;

        

         A51: p <> (f /. (i -' 1)) by A4, A6, A39, A42, GOBOARD7: 29;

        

         A52: not (( LSeg (f,(i -' 1))) is horizontal & ( LSeg (f,i)) is horizontal)

        proof

          assume ( LSeg (f,(i -' 1))) is horizontal & ( LSeg (f,i)) is horizontal;

          then

           A53: (p `2 ) = ((f /. (i + 1)) `2 ) & (p `2 ) = ((f /. (i -' 1)) `2 ) by A50, A49, A41, A45, SPPOL_1:def 2;

          

           A54: ((f /. (i + 1)) `1 ) <= ((f /. (i -' 1)) `1 ) or ((f /. (i + 1)) `1 ) >= ((f /. (i -' 1)) `1 );

          

           A55: (p `1 ) <= ((f /. (i + 1)) `1 ) & (p `1 ) <= ((f /. (i -' 1)) `1 ) by A7, A43, A47, PSCOMP_1: 24;

          ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) & ( LSeg (f,(i -' 1))) = ( LSeg ((f /. i),(f /. (i -' 1)))) by A37, A38, A39, A40, A44, TOPREAL1:def 3;

          then (f /. (i -' 1)) in ( LSeg (f,i)) or (f /. (i + 1)) in ( LSeg (f,(i -' 1))) by A6, A53, A55, A54, GOBOARD7: 8;

          then (f /. (i -' 1)) in (( LSeg (f,(i -' 1))) /\ ( LSeg (f,i))) or (f /. (i + 1)) in (( LSeg (f,(i -' 1))) /\ ( LSeg (f,i))) by A41, A45, XBOOLE_0:def 4;

          then (((i -' 1) + 1) + 1) = ((i -' 1) + (1 + 1)) & (( LSeg (f,(i -' 1))) /\ ( LSeg (f,i))) <> {(f /. i)} by A6, A51, A48, TARSKI:def 1;

          hence contradiction by A39, A40, A44, TOPREAL1:def 6;

        end;

        now

          per cases by A52, SPPOL_1: 19;

            suppose ( LSeg (f,(i -' 1))) is vertical;

            then

             A56: (p `1 ) = ((f /. (i -' 1)) `1 ) by A50, A41, SPPOL_1:def 3;

            then

             A57: (f /. (i -' 1)) in ( W-most ( L~ f)) by A2, A7, A42, Th12, GOBOARD1: 1;

            then

             A58: ((f /. (i -' 1)) `2 ) >= (p `2 ) by PSCOMP_1: 31;

            ((f /. (i -' 1)) `2 ) <> (p `2 ) by A4, A6, A39, A42, A56, GOBOARD7: 29, TOPREAL3: 6;

            then

             A59: ((f /. (i -' 1)) `2 ) > (p `2 ) by A58, XXREAL_0: 1;

            ((f /. (i -' 1)) `2 ) <= (( W-max ( L~ f)) `2 ) by A57, PSCOMP_1: 31;

            hence thesis by A59, XXREAL_0: 2;

          end;

            suppose ( LSeg (f,i)) is vertical;

            then

             A60: (p `1 ) = ((f /. (i + 1)) `1 ) by A49, A45, SPPOL_1:def 3;

            then

             A61: (f /. (i + 1)) in ( W-most ( L~ f)) by A2, A7, A46, Th12, GOBOARD1: 1;

            then

             A62: ((f /. (i + 1)) `2 ) >= (p `2 ) by PSCOMP_1: 31;

            ((f /. (i + 1)) `2 ) <> (p `2 ) by A4, A6, A46, A60, GOBOARD7: 29, TOPREAL3: 6;

            then

             A63: ((f /. (i + 1)) `2 ) > (p `2 ) by A62, XXREAL_0: 1;

            ((f /. (i + 1)) `2 ) <= (( W-max ( L~ f)) `2 ) by A61, PSCOMP_1: 31;

            hence thesis by A63, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: SPRECT_2:58

    

     Th58: ( W-min ( L~ f)) <> ( W-max ( L~ f))

    proof

      (( W-min ( L~ f)) `2 ) < (( W-max ( L~ f)) `2 ) by Th57;

      hence thesis;

    end;

    theorem :: SPRECT_2:59

    

     Th59: ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) misses ( LSeg (( N-max ( L~ f)),( NE-corner ( L~ f))))

    proof

      

       A1: (( N-min ( L~ f)) `2 ) = (( N-max ( L~ f)) `2 ) by PSCOMP_1: 37;

      assume ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) meets ( LSeg (( N-max ( L~ f)),( NE-corner ( L~ f))));

      then

      consider p be object such that

       A2: p in ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) and

       A3: p in ( LSeg (( N-max ( L~ f)),( NE-corner ( L~ f)))) by XBOOLE_0: 3;

      reconsider p as Point of ( TOP-REAL 2) by A2;

      (( N-max ( L~ f)) `1 ) <= (( NE-corner ( L~ f)) `1 ) by PSCOMP_1: 38;

      then

       A4: (( N-max ( L~ f)) `1 ) <= (p `1 ) by A3, TOPREAL1: 3;

      (( NW-corner ( L~ f)) `1 ) <= (( N-min ( L~ f)) `1 ) by PSCOMP_1: 38;

      then (p `1 ) <= (( N-min ( L~ f)) `1 ) by A2, TOPREAL1: 3;

      then

       A5: (( N-min ( L~ f)) `1 ) >= (( N-max ( L~ f)) `1 ) by A4, XXREAL_0: 2;

      (( N-min ( L~ f)) `1 ) <= (( N-max ( L~ f)) `1 ) by PSCOMP_1: 38;

      then (( N-min ( L~ f)) `1 ) = (( N-max ( L~ f)) `1 ) by A5, XXREAL_0: 1;

      hence contradiction by A1, Th52, TOPREAL3: 6;

    end;

    theorem :: SPRECT_2:60

    

     Th60: for f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st f is being_S-Seq & p <> (f /. 1) & ((p `1 ) = ((f /. 1) `1 ) or (p `2 ) = ((f /. 1) `2 )) & (( LSeg (p,(f /. 1))) /\ ( L~ f)) = {(f /. 1)} holds ( <*p*> ^ f) is S-Sequence_in_R2

    proof

      let f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) such that

       A1: f is being_S-Seq and

       A2: p <> (f /. 1) and

       A3: (p `1 ) = ((f /. 1) `1 ) or (p `2 ) = ((f /. 1) `2 ) and

       A4: (( LSeg (p,(f /. 1))) /\ ( L~ f)) = {(f /. 1)};

      reconsider f as S-Sequence_in_R2 by A1;

      

       A5: ( len f) >= (1 + 1) by TOPREAL1:def 8;

      then

       A6: (f /. 1) in ( LSeg (f,1)) by TOPREAL1: 21;

      set g = ( <*p*> ^ f);

      ( len g) = (( len <*p*>) + ( len f)) by FINSEQ_1: 22;

      then ( len g) >= ( len f) by NAT_1: 11;

      then

       A7: ( len g) >= 2 by A5, XXREAL_0: 2;

      now

        assume

         A8: p in ( rng f);

        ( rng f) c= ( L~ f) & p in ( LSeg (p,(f /. 1))) by A5, RLTOPSP1: 68, SPPOL_2: 18;

        then p in {(f /. 1)} by A4, A8, XBOOLE_0:def 4;

        hence contradiction by A2, TARSKI:def 1;

      end;

      then {p} misses ( rng f) by ZFMISC_1: 50;

      then <*p*> is one-to-one & ( rng <*p*>) misses ( rng f) by FINSEQ_1: 39, FINSEQ_3: 93;

      then

       A9: g is one-to-one by FINSEQ_3: 91;

      ( L~ <*p*>) = {} by SPPOL_2: 12;

      then (( L~ <*p*>) /\ ( L~ f)) = {} ;

      then

       A10: ( L~ <*p*>) misses ( L~ f);

      

       A11: 1 in ( dom f) by FINSEQ_5: 6;

       A12:

      now

        let i such that

         A13: (1 + 1) <= i and

         A14: (i + 1) <= ( len f);

        

         A15: 2 in ( dom f) by A5, FINSEQ_3: 25;

        now

          assume (f /. 1) in ( LSeg (f,i));

          then

           A16: (f /. 1) in (( LSeg (f,1)) /\ ( LSeg (f,i))) by A6, XBOOLE_0:def 4;

          then

           A17: ( LSeg (f,1)) meets ( LSeg (f,i));

          now

            per cases by A13, XXREAL_0: 1;

              case

               A18: i = (1 + 1);

              then (( LSeg (f,1)) /\ ( LSeg (f,(1 + 1)))) = {(f /. 2)} by A14, TOPREAL1:def 6;

              hence (f /. 1) = (f /. 2) by A16, A18, TARSKI:def 1;

            end;

              case i > (1 + 1);

              hence contradiction by A17, TOPREAL1:def 7;

            end;

          end;

          

          then (f . 1) = (f /. 2) by A11, PARTFUN1:def 6

          .= (f . 2) by A15, PARTFUN1:def 6;

          hence contradiction by A11, A15, FUNCT_1:def 4;

        end;

        then not (f /. 1) in (( LSeg (f,i)) /\ ( LSeg (p,(f /. 1)))) by XBOOLE_0:def 4;

        then

         A19: (( LSeg (f,i)) /\ ( LSeg (p,(f /. 1)))) <> {(f /. 1)} by TARSKI:def 1;

        (( LSeg (f,i)) /\ ( LSeg (p,(f /. 1)))) c= {(f /. 1)} by A4, TOPREAL3: 19, XBOOLE_1: 26;

        then (( LSeg (f,i)) /\ ( LSeg (p,(f /. 1)))) = {} by A19, ZFMISC_1: 33;

        hence ( LSeg (f,i)) misses ( LSeg (p,(f /. 1)));

      end;

      

       A20: ( len <*p*>) = 1 by FINSEQ_1: 39;

      then

       A21: <*p*> is s.n.c. & ( <*p*> /. ( len <*p*>)) = p by FINSEQ_4: 16, SPPOL_2: 33;

       A22:

      now

        let i such that 1 <= i;

        

         A23: 2 <= (i + 2) by NAT_1: 11;

        assume (i + 2) <= ( len <*p*>);

        hence ( LSeg ( <*p*>,i)) misses ( LSeg (p,(f /. 1))) by A20, A23, XXREAL_0: 2;

      end;

      (( LSeg (p,(f /. 1))) /\ ( LSeg (f,1))) = {(f /. 1)} by A4, A6, TOPREAL3: 19, ZFMISC_1: 124;

      then g is unfolded s.n.c. special by A3, A21, A10, A22, A12, GOBOARD2: 8, SPPOL_2: 29, SPPOL_2: 36;

      hence thesis by A9, A7, TOPREAL1:def 8;

    end;

    theorem :: SPRECT_2:61

    

     Th61: for f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st f is being_S-Seq & p <> (f /. ( len f)) & ((p `1 ) = ((f /. ( len f)) `1 ) or (p `2 ) = ((f /. ( len f)) `2 )) & (( LSeg (p,(f /. ( len f)))) /\ ( L~ f)) = {(f /. ( len f))} holds (f ^ <*p*>) is S-Sequence_in_R2

    proof

      let f be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) such that

       A1: f is being_S-Seq and

       A2: p <> (f /. ( len f)) & ((p `1 ) = ((f /. ( len f)) `1 ) or (p `2 ) = ((f /. ( len f)) `2 )) and

       A3: (( LSeg (p,(f /. ( len f)))) /\ ( L~ f)) = {(f /. ( len f))};

      set g = <*(f /. ( len f)), p*>;

      

       A4: g is being_S-Seq by A2, SPPOL_2: 43;

      

       AB: ( len g) = (1 + 1) by FINSEQ_1: 44;

      then

       AA: 2 in ( dom g) by FINSEQ_3: 25;

      

      then

       A5: ( mid (g,2,( len g))) = <*(g . 2)*> by JORDAN4: 15, AB

      .= <*(g /. 2)*> by AA, PARTFUN1:def 6

      .= <*p*> by FINSEQ_4: 17;

      reconsider f9 = f as S-Sequence_in_R2 by A1;

      

       A6: ( len f9) in ( dom f9) by FINSEQ_5: 6;

      

       A7: (g . 1) = (f /. ( len f)) by FINSEQ_1: 44

      .= (f . ( len f)) by A6, PARTFUN1:def 6;

      (( L~ f) /\ ( L~ g)) = {(f /. ( len f))} by A3, SPPOL_2: 21

      .= {(f . ( len f))} by A6, PARTFUN1:def 6;

      hence thesis by A1, A7, A4, A5, JORDAN3: 38;

    end;

    begin

    theorem :: SPRECT_2:62

    

     Th62: for i, j st i in ( dom f) & j in ( dom f) & ( mid (f,i,j)) is S-Sequence_in_R2 & (f /. j) = ( N-max ( L~ f)) & ( N-max ( L~ f)) <> ( NE-corner ( L~ f)) holds (( mid (f,i,j)) ^ <*( NE-corner ( L~ f))*>) is S-Sequence_in_R2

    proof

      set p = ( NE-corner ( L~ f));

      let i, j such that

       A1: i in ( dom f) and

       A2: j in ( dom f) and

       A3: ( mid (f,i,j)) is S-Sequence_in_R2 and

       A4: (f /. j) = ( N-max ( L~ f)) and

       A5: ( N-max ( L~ f)) <> ( NE-corner ( L~ f));

      

       A6: 1 <= i & i <= ( len f) by A1, FINSEQ_3: 25;

      

       A7: (( mid (f,i,j)) /. ( len ( mid (f,i,j)))) = ( N-max ( L~ f)) by A1, A2, A4, Th9;

      then

       A8: (p `2 ) = ((( mid (f,i,j)) /. ( len ( mid (f,i,j)))) `2 ) by PSCOMP_1: 37;

      

       A9: 1 <= j & j <= ( len f) by A2, FINSEQ_3: 25;

      ( len ( mid (f,i,j))) >= 2 by A3, TOPREAL1:def 8;

      then (( LSeg (( NE-corner ( L~ f)),( N-max ( L~ f)))) /\ ( L~ f)) = {( N-max ( L~ f))} & ( N-max ( L~ f)) in ( L~ ( mid (f,i,j))) by A7, JORDAN3: 1, PSCOMP_1: 43;

      then (( LSeg (p,(( mid (f,i,j)) /. ( len ( mid (f,i,j)))))) /\ ( L~ ( mid (f,i,j)))) = {(( mid (f,i,j)) /. ( len ( mid (f,i,j))))} by A7, A6, A9, JORDAN4: 35, ZFMISC_1: 124;

      hence thesis by A3, A5, A7, A8, Th61;

    end;

    theorem :: SPRECT_2:63

    for i, j st i in ( dom f) & j in ( dom f) & ( mid (f,i,j)) is S-Sequence_in_R2 & (f /. j) = ( E-max ( L~ f)) & ( E-max ( L~ f)) <> ( NE-corner ( L~ f)) holds (( mid (f,i,j)) ^ <*( NE-corner ( L~ f))*>) is S-Sequence_in_R2

    proof

      set p = ( NE-corner ( L~ f));

      let i, j such that

       A1: i in ( dom f) and

       A2: j in ( dom f) and

       A3: ( mid (f,i,j)) is S-Sequence_in_R2 and

       A4: (f /. j) = ( E-max ( L~ f)) and

       A5: ( E-max ( L~ f)) <> ( NE-corner ( L~ f));

      

       A6: 1 <= i & i <= ( len f) by A1, FINSEQ_3: 25;

      

       A7: (( mid (f,i,j)) /. ( len ( mid (f,i,j)))) = ( E-max ( L~ f)) by A1, A2, A4, Th9;

      then

       A8: (p `1 ) = ((( mid (f,i,j)) /. ( len ( mid (f,i,j)))) `1 ) by PSCOMP_1: 45;

      

       A9: 1 <= j & j <= ( len f) by A2, FINSEQ_3: 25;

      ( len ( mid (f,i,j))) >= 2 by A3, TOPREAL1:def 8;

      then (( LSeg (( NE-corner ( L~ f)),( E-max ( L~ f)))) /\ ( L~ f)) = {( E-max ( L~ f))} & ( E-max ( L~ f)) in ( L~ ( mid (f,i,j))) by A7, JORDAN3: 1, PSCOMP_1: 51;

      then (( LSeg (p,(( mid (f,i,j)) /. ( len ( mid (f,i,j)))))) /\ ( L~ ( mid (f,i,j)))) = {(( mid (f,i,j)) /. ( len ( mid (f,i,j))))} by A7, A6, A9, JORDAN4: 35, ZFMISC_1: 124;

      hence thesis by A3, A5, A7, A8, Th61;

    end;

    theorem :: SPRECT_2:64

    

     Th64: for i, j st i in ( dom f) & j in ( dom f) & ( mid (f,i,j)) is S-Sequence_in_R2 & (f /. j) = ( S-max ( L~ f)) & ( S-max ( L~ f)) <> ( SE-corner ( L~ f)) holds (( mid (f,i,j)) ^ <*( SE-corner ( L~ f))*>) is S-Sequence_in_R2

    proof

      set p = ( SE-corner ( L~ f));

      let i, j such that

       A1: i in ( dom f) and

       A2: j in ( dom f) and

       A3: ( mid (f,i,j)) is S-Sequence_in_R2 and

       A4: (f /. j) = ( S-max ( L~ f)) and

       A5: ( S-max ( L~ f)) <> ( SE-corner ( L~ f));

      

       A6: 1 <= i & i <= ( len f) by A1, FINSEQ_3: 25;

      

       A7: (( mid (f,i,j)) /. ( len ( mid (f,i,j)))) = ( S-max ( L~ f)) by A1, A2, A4, Th9;

      then

       A8: (p `2 ) = ((( mid (f,i,j)) /. ( len ( mid (f,i,j)))) `2 ) by PSCOMP_1: 53;

      

       A9: 1 <= j & j <= ( len f) by A2, FINSEQ_3: 25;

      ( len ( mid (f,i,j))) >= 2 by A3, TOPREAL1:def 8;

      then (( LSeg (( SE-corner ( L~ f)),( S-max ( L~ f)))) /\ ( L~ f)) = {( S-max ( L~ f))} & ( S-max ( L~ f)) in ( L~ ( mid (f,i,j))) by A7, JORDAN3: 1, PSCOMP_1: 59;

      then (( LSeg (p,(( mid (f,i,j)) /. ( len ( mid (f,i,j)))))) /\ ( L~ ( mid (f,i,j)))) = {(( mid (f,i,j)) /. ( len ( mid (f,i,j))))} by A7, A6, A9, JORDAN4: 35, ZFMISC_1: 124;

      hence thesis by A3, A5, A7, A8, Th61;

    end;

    theorem :: SPRECT_2:65

    

     Th65: for i, j st i in ( dom f) & j in ( dom f) & ( mid (f,i,j)) is S-Sequence_in_R2 & (f /. j) = ( E-max ( L~ f)) & ( E-max ( L~ f)) <> ( NE-corner ( L~ f)) holds (( mid (f,i,j)) ^ <*( NE-corner ( L~ f))*>) is S-Sequence_in_R2

    proof

      set p = ( NE-corner ( L~ f));

      let i, j such that

       A1: i in ( dom f) and

       A2: j in ( dom f) and

       A3: ( mid (f,i,j)) is S-Sequence_in_R2 and

       A4: (f /. j) = ( E-max ( L~ f)) and

       A5: ( E-max ( L~ f)) <> ( NE-corner ( L~ f));

      

       A6: 1 <= i & i <= ( len f) by A1, FINSEQ_3: 25;

      

       A7: (( mid (f,i,j)) /. ( len ( mid (f,i,j)))) = ( E-max ( L~ f)) by A1, A2, A4, Th9;

      then

       A8: (p `1 ) = ((( mid (f,i,j)) /. ( len ( mid (f,i,j)))) `1 ) by PSCOMP_1: 45;

      

       A9: 1 <= j & j <= ( len f) by A2, FINSEQ_3: 25;

      ( len ( mid (f,i,j))) >= 2 by A3, TOPREAL1:def 8;

      then (( LSeg (( NE-corner ( L~ f)),( E-max ( L~ f)))) /\ ( L~ f)) = {( E-max ( L~ f))} & ( E-max ( L~ f)) in ( L~ ( mid (f,i,j))) by A7, JORDAN3: 1, PSCOMP_1: 51;

      then (( LSeg (p,(( mid (f,i,j)) /. ( len ( mid (f,i,j)))))) /\ ( L~ ( mid (f,i,j)))) = {(( mid (f,i,j)) /. ( len ( mid (f,i,j))))} by A7, A6, A9, JORDAN4: 35, ZFMISC_1: 124;

      hence thesis by A3, A5, A7, A8, Th61;

    end;

    theorem :: SPRECT_2:66

    

     Th66: for i, j st i in ( dom f) & j in ( dom f) & ( mid (f,i,j)) is S-Sequence_in_R2 & (f /. i) = ( N-min ( L~ f)) & ( N-min ( L~ f)) <> ( NW-corner ( L~ f)) holds ( <*( NW-corner ( L~ f))*> ^ ( mid (f,i,j))) is S-Sequence_in_R2

    proof

      set p = ( NW-corner ( L~ f));

      let i, j such that

       A1: i in ( dom f) and

       A2: j in ( dom f) and

       A3: ( mid (f,i,j)) is S-Sequence_in_R2 and

       A4: (f /. i) = ( N-min ( L~ f)) and

       A5: ( N-min ( L~ f)) <> ( NW-corner ( L~ f));

      

       A6: 1 <= i & i <= ( len f) by A1, FINSEQ_3: 25;

      

       A7: (( mid (f,i,j)) /. 1) = ( N-min ( L~ f)) by A1, A2, A4, Th8;

      then

       A8: (p `2 ) = ((( mid (f,i,j)) /. 1) `2 ) by PSCOMP_1: 37;

      

       A9: 1 <= j & j <= ( len f) by A2, FINSEQ_3: 25;

      ( len ( mid (f,i,j))) >= 2 by A3, TOPREAL1:def 8;

      then (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ f)) = {( N-min ( L~ f))} & ( N-min ( L~ f)) in ( L~ ( mid (f,i,j))) by A7, JORDAN3: 1, PSCOMP_1: 43;

      then (( LSeg (p,(( mid (f,i,j)) /. 1))) /\ ( L~ ( mid (f,i,j)))) = {(( mid (f,i,j)) /. 1)} by A7, A6, A9, JORDAN4: 35, ZFMISC_1: 124;

      hence thesis by A3, A5, A7, A8, Th60;

    end;

    theorem :: SPRECT_2:67

    

     Th67: for i, j st i in ( dom f) & j in ( dom f) & ( mid (f,i,j)) is S-Sequence_in_R2 & (f /. i) = ( W-min ( L~ f)) & ( W-min ( L~ f)) <> ( SW-corner ( L~ f)) holds ( <*( SW-corner ( L~ f))*> ^ ( mid (f,i,j))) is S-Sequence_in_R2

    proof

      set p = ( SW-corner ( L~ f));

      let i, j such that

       A1: i in ( dom f) and

       A2: j in ( dom f) and

       A3: ( mid (f,i,j)) is S-Sequence_in_R2 and

       A4: (f /. i) = ( W-min ( L~ f)) and

       A5: ( W-min ( L~ f)) <> ( SW-corner ( L~ f));

      

       A6: 1 <= i & i <= ( len f) by A1, FINSEQ_3: 25;

      

       A7: (( mid (f,i,j)) /. 1) = ( W-min ( L~ f)) by A1, A2, A4, Th8;

      then

       A8: (p `1 ) = ((( mid (f,i,j)) /. 1) `1 ) by PSCOMP_1: 29;

      

       A9: 1 <= j & j <= ( len f) by A2, FINSEQ_3: 25;

      ( len ( mid (f,i,j))) >= 2 by A3, TOPREAL1:def 8;

      then (( LSeg (( SW-corner ( L~ f)),( W-min ( L~ f)))) /\ ( L~ f)) = {( W-min ( L~ f))} & ( W-min ( L~ f)) in ( L~ ( mid (f,i,j))) by A7, JORDAN3: 1, PSCOMP_1: 35;

      then (( LSeg (p,(( mid (f,i,j)) /. 1))) /\ ( L~ ( mid (f,i,j)))) = {(( mid (f,i,j)) /. 1)} by A7, A6, A9, JORDAN4: 35, ZFMISC_1: 124;

      hence thesis by A3, A5, A7, A8, Th60;

    end;

    

     Lm1: for i, j st i in ( dom f) & j in ( dom f) & ( mid (f,i,j)) is S-Sequence_in_R2 & (f /. i) = ( N-min ( L~ f)) & ( N-min ( L~ f)) <> ( NW-corner ( L~ f)) & (f /. j) = ( N-max ( L~ f)) & ( N-max ( L~ f)) <> ( NE-corner ( L~ f)) holds (( <*( NW-corner ( L~ f))*> ^ ( mid (f,i,j))) ^ <*( NE-corner ( L~ f))*>) is S-Sequence_in_R2

    proof

      set p = ( NW-corner ( L~ f)), q = ( NE-corner ( L~ f));

      let i, j such that

       A1: i in ( dom f) and

       A2: j in ( dom f) and

       A3: ( mid (f,i,j)) is S-Sequence_in_R2 and

       A4: (f /. i) = ( N-min ( L~ f)) and

       A5: ( N-min ( L~ f)) <> ( NW-corner ( L~ f)) and

       A6: (f /. j) = ( N-max ( L~ f)) and

       A7: ( N-max ( L~ f)) <> ( NE-corner ( L~ f));

      set g = ( <*( NW-corner ( L~ f))*> ^ ( mid (f,i,j)));

      

       A8: g is S-Sequence_in_R2 by A1, A2, A3, A4, A5, Th66;

      ( len g) = (( len <*( NW-corner ( L~ f))*>) + ( len ( mid (f,i,j)))) & ( len ( mid (f,i,j))) in ( dom ( mid (f,i,j))) by A3, FINSEQ_1: 22, FINSEQ_5: 6;

      then

       A9: (g /. ( len g)) = (( mid (f,i,j)) /. ( len ( mid (f,i,j)))) by FINSEQ_4: 69;

      then

       A10: (g /. ( len g)) = ( N-max ( L~ f)) by A1, A2, A6, Th9;

      then

       A11: (q `2 ) = ((g /. ( len g)) `2 ) by PSCOMP_1: 37;

      (( mid (f,i,j)) /. 1) = (f /. i) by A1, A2, Th8;

      then

       A12: ( L~ g) = (( LSeg (p,( N-min ( L~ f)))) \/ ( L~ ( mid (f,i,j)))) by A3, A4, SPPOL_2: 20;

      

       A13: 1 <= j & j <= ( len f) by A2, FINSEQ_3: 25;

      

       A14: 1 <= i & i <= ( len f) by A1, FINSEQ_3: 25;

      ( len ( mid (f,i,j))) >= 2 by A3, TOPREAL1:def 8;

      then

       A15: (( LSeg (( NE-corner ( L~ f)),( N-max ( L~ f)))) /\ ( L~ f)) = {( N-max ( L~ f))} & ( N-max ( L~ f)) in ( L~ ( mid (f,i,j))) by A9, A10, JORDAN3: 1, PSCOMP_1: 43;

      ( LSeg ((g /. ( len g)),q)) misses ( LSeg (p,( N-min ( L~ f)))) by A10, Th59;

      then (( LSeg (q,(g /. ( len g)))) /\ ( LSeg (p,( N-min ( L~ f))))) = {} ;

      

      then (( LSeg (q,(g /. ( len g)))) /\ ( L~ g)) = ((( LSeg (q,(g /. ( len g)))) /\ ( L~ ( mid (f,i,j)))) \/ {} ) by A12, XBOOLE_1: 23

      .= {(g /. ( len g))} by A10, A15, A14, A13, JORDAN4: 35, ZFMISC_1: 124;

      hence thesis by A7, A8, A10, A11, Th61;

    end;

    registration

      let f be non constant standard special_circular_sequence;

      cluster ( L~ f) -> being_simple_closed_curve;

      coherence by JORDAN4: 51;

    end

    

     Lm2: ( LSeg (( S-max ( L~ f)),( SE-corner ( L~ f)))) misses ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f))))

    proof

      

       A1: (( NW-corner ( L~ f)) `2 ) = ( N-bound ( L~ f)) & (( N-min ( L~ f)) `2 ) = ( N-bound ( L~ f)) by EUCLID: 52;

      assume ( LSeg (( S-max ( L~ f)),( SE-corner ( L~ f)))) meets ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f))));

      then (( LSeg (( S-max ( L~ f)),( SE-corner ( L~ f)))) /\ ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f))))) <> {} ;

      then

      consider x be object such that

       A2: x in (( LSeg (( S-max ( L~ f)),( SE-corner ( L~ f)))) /\ ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f))))) by XBOOLE_0:def 1;

      reconsider p = x as Point of ( TOP-REAL 2) by A2;

      p in ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) by A2, XBOOLE_0:def 4;

      then ( N-bound ( L~ f)) <= (p `2 ) & (p `2 ) <= ( N-bound ( L~ f)) by A1, TOPREAL1: 4;

      then

       A3: (p `2 ) = ( N-bound ( L~ f)) by XXREAL_0: 1;

      

       A4: (( SE-corner ( L~ f)) `2 ) = ( S-bound ( L~ f)) & (( S-max ( L~ f)) `2 ) = ( S-bound ( L~ f)) by EUCLID: 52;

      x in ( LSeg (( S-max ( L~ f)),( SE-corner ( L~ f)))) by A2, XBOOLE_0:def 4;

      then (p `2 ) <= ( S-bound ( L~ f)) by A4, TOPREAL1: 4;

      hence contradiction by A3, TOPREAL5: 16;

    end;

    

     Lm3: for i, j st i in ( dom f) & j in ( dom f) & ( mid (f,i,j)) is S-Sequence_in_R2 & (f /. i) = ( N-min ( L~ f)) & ( N-min ( L~ f)) <> ( NW-corner ( L~ f)) & (f /. j) = ( S-max ( L~ f)) & ( S-max ( L~ f)) <> ( SE-corner ( L~ f)) holds (( <*( NW-corner ( L~ f))*> ^ ( mid (f,i,j))) ^ <*( SE-corner ( L~ f))*>) is S-Sequence_in_R2

    proof

      set p = ( NW-corner ( L~ f)), q = ( SE-corner ( L~ f));

      let i, j such that

       A1: i in ( dom f) and

       A2: j in ( dom f) and

       A3: ( mid (f,i,j)) is S-Sequence_in_R2 and

       A4: (f /. i) = ( N-min ( L~ f)) and

       A5: ( N-min ( L~ f)) <> ( NW-corner ( L~ f)) and

       A6: (f /. j) = ( S-max ( L~ f)) and

       A7: ( S-max ( L~ f)) <> ( SE-corner ( L~ f));

      set g = ( <*( NW-corner ( L~ f))*> ^ ( mid (f,i,j)));

      

       A8: g is S-Sequence_in_R2 by A1, A2, A3, A4, A5, Th66;

      ( len g) = (( len <*( NW-corner ( L~ f))*>) + ( len ( mid (f,i,j)))) & ( len ( mid (f,i,j))) in ( dom ( mid (f,i,j))) by A3, FINSEQ_1: 22, FINSEQ_5: 6;

      then

       A9: (g /. ( len g)) = (( mid (f,i,j)) /. ( len ( mid (f,i,j)))) by FINSEQ_4: 69;

      then

       A10: (g /. ( len g)) = ( S-max ( L~ f)) by A1, A2, A6, Th9;

      then

       A11: (q `2 ) = ((g /. ( len g)) `2 ) by PSCOMP_1: 53;

      (( mid (f,i,j)) /. 1) = (f /. i) by A1, A2, Th8;

      then

       A12: ( L~ g) = (( LSeg (p,( N-min ( L~ f)))) \/ ( L~ ( mid (f,i,j)))) by A3, A4, SPPOL_2: 20;

      

       A13: 1 <= j & j <= ( len f) by A2, FINSEQ_3: 25;

      

       A14: 1 <= i & i <= ( len f) by A1, FINSEQ_3: 25;

      ( len ( mid (f,i,j))) >= 2 by A3, TOPREAL1:def 8;

      then

       A15: (( LSeg (( SE-corner ( L~ f)),( S-max ( L~ f)))) /\ ( L~ f)) = {( S-max ( L~ f))} & ( S-max ( L~ f)) in ( L~ ( mid (f,i,j))) by A9, A10, JORDAN3: 1, PSCOMP_1: 59;

      ( LSeg ((g /. ( len g)),q)) misses ( LSeg (p,( N-min ( L~ f)))) by A10, Lm2;

      then (( LSeg (q,(g /. ( len g)))) /\ ( LSeg (p,( N-min ( L~ f))))) = {} ;

      

      then (( LSeg (q,(g /. ( len g)))) /\ ( L~ g)) = ((( LSeg (q,(g /. ( len g)))) /\ ( L~ ( mid (f,i,j)))) \/ {} ) by A12, XBOOLE_1: 23

      .= {(g /. ( len g))} by A10, A15, A14, A13, JORDAN4: 35, ZFMISC_1: 124;

      hence thesis by A7, A8, A10, A11, Th61;

    end;

    begin

    theorem :: SPRECT_2:68

    

     Th68: (f /. 1) = ( N-min ( L~ f)) implies (( N-min ( L~ f)) .. f) < (( N-max ( L~ f)) .. f)

    proof

      assume (f /. 1) = ( N-min ( L~ f));

      then

       A1: (( N-min ( L~ f)) .. f) = 1 by FINSEQ_6: 43;

      

       A2: ( N-max ( L~ f)) in ( rng f) by Th40;

      then (( N-max ( L~ f)) .. f) in ( dom f) by FINSEQ_4: 20;

      then

       A3: (( N-max ( L~ f)) .. f) >= 1 by FINSEQ_3: 25;

      ( N-min ( L~ f)) in ( rng f) by Th39;

      then (( N-min ( L~ f)) .. f) <> (( N-max ( L~ f)) .. f) by A2, Th52, FINSEQ_5: 9;

      hence thesis by A3, A1, XXREAL_0: 1;

    end;

    theorem :: SPRECT_2:69

    (f /. 1) = ( N-min ( L~ f)) implies (( N-max ( L~ f)) .. f) > 1

    proof

      assume

       A1: (f /. 1) = ( N-min ( L~ f));

      then (( N-min ( L~ f)) .. f) = 1 by FINSEQ_6: 43;

      hence thesis by A1, Th68;

    end;

    

     Lm4: (f /. 1) = ( N-min ( L~ f)) implies (( N-min ( L~ f)) .. f) < (( E-max ( L~ f)) .. f)

    proof

      

       A1: ( N-min ( L~ f)) in ( rng f) by Th39;

      assume (f /. 1) = ( N-min ( L~ f));

      then

       A2: (( N-min ( L~ f)) .. f) = 1 by FINSEQ_6: 43;

      (( N-max ( L~ f)) `1 ) <= (( NE-corner ( L~ f)) `1 ) by PSCOMP_1: 38;

      then (( N-max ( L~ f)) `1 ) <= ( E-bound ( L~ f)) by EUCLID: 52;

      then (( N-min ( L~ f)) `1 ) < ( E-bound ( L~ f)) by Th51, XXREAL_0: 2;

      then

       A3: (( N-min ( L~ f)) `1 ) < (( E-max ( L~ f)) `1 ) by EUCLID: 52;

      

       A4: ( E-max ( L~ f)) in ( rng f) by Th46;

      then (( E-max ( L~ f)) .. f) >= 1 by FINSEQ_4: 21;

      hence thesis by A4, A1, A3, A2, FINSEQ_5: 9, XXREAL_0: 1;

    end;

    reserve z for clockwise_oriented non constant standard special_circular_sequence;

    

     Lm5: (z /. 1) = ( N-min ( L~ z)) implies (( N-max ( L~ z)) .. z) < (( S-max ( L~ z)) .. z)

    proof

      set i1 = (( N-max ( L~ z)) .. z), i2 = (( S-max ( L~ z)) .. z);

      assume that

       A1: (z /. 1) = ( N-min ( L~ z)) and

       A2: i1 >= i2;

      

       A3: ( N-min ( L~ z)) <> ( N-max ( L~ z)) by Th52;

      

       A4: ( S-max ( L~ z)) in ( rng z) by Th42;

      then

       A5: i2 in ( dom z) by FINSEQ_4: 20;

      then

       A6: i2 <= ( len z) by FINSEQ_3: 25;

      

       A7: (z /. i2) = (z . i2) by A5, PARTFUN1:def 6

      .= ( S-max ( L~ z)) by A4, FINSEQ_4: 19;

      then

       A8: ((z /. i2) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      

       A9: 1 <= i2 by A5, FINSEQ_3: 25;

      

       A10: i2 <> 0 by A5, FINSEQ_3: 25;

      ((z /. 1) `2 ) = ( N-bound ( L~ z)) by A1, EUCLID: 52;

      then

       A11: i2 <> 1 by A8, TOPREAL5: 16;

      (z /. 2) in ( N-most ( L~ z)) by A1, Th30;

      

      then

       A12: ((z /. 2) `2 ) = (( N-min ( L~ z)) `2 ) by PSCOMP_1: 39

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

      then i2 <> 2 by A8, TOPREAL5: 16;

      then i2 <> 0 & ... & i2 <> 2 by A10, A11;

      then

       A13: i2 > 2;

      then

      reconsider h = ( mid (z,i2,2)) as S-Sequence_in_R2 by A6, Th37;

      

       A14: 2 <= ( len z) by NAT_D: 60;

      then

       A15: 2 in ( dom z) by FINSEQ_3: 25;

      then

       A16: ((h /. ( len h)) `2 ) = ( N-bound ( L~ z)) by A5, A12, Th9;

      (h /. 1) = ( S-max ( L~ z)) by A5, A7, A15, Th8;

      then

       A17: ((h /. 1) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      h is_in_the_area_of z by A5, A15, Th21, Th22;

      then

       A18: h is_a_v.c._for z by A17, A16;

      

       A19: ( N-max ( L~ z)) in ( rng z) by Th40;

      then

       A20: i1 in ( dom z) by FINSEQ_4: 20;

      

      then

       A21: (z /. i1) = (z . i1) by PARTFUN1:def 6

      .= ( N-max ( L~ z)) by A19, FINSEQ_4: 19;

      

       A22: i1 <= ( len z) by A20, FINSEQ_3: 25;

      (z /. ( len z)) = ( N-min ( L~ z)) by A1, FINSEQ_6:def 1;

      then

       A23: i1 < ( len z) by A22, A21, A3, XXREAL_0: 1;

      then (i1 + 1) <= ( len z) by NAT_1: 13;

      then (( len z) - i1) >= 1 by XREAL_1: 19;

      then (( len z) -' i1) >= 1 by NAT_D: 39;

      then

       A24: ((( len z) -' i1) + 1) >= (1 + 1) by XREAL_1: 6;

      (( N-max ( L~ z)) `2 ) = ( N-bound ( L~ z)) & (( S-max ( L~ z)) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      then (z /. i1) <> (z /. i2) by A7, A21, TOPREAL5: 16;

      then

       A25: i1 > i2 by A2, XXREAL_0: 1;

      then i1 > 1 by A9, XXREAL_0: 2;

      then

      reconsider M = ( mid (z,( len z),i1)) as S-Sequence_in_R2 by A23, Th37;

      

       A26: 1 in ( dom M) by FINSEQ_5: 6;

      

       A27: ( len z) in ( dom z) by FINSEQ_5: 6;

      

      then

       A28: (M /. ( len M)) = (z /. i1) by A20, Th9

      .= ( N-max ( L~ z)) by A19, FINSEQ_5: 38;

      

       A29: ( L~ M) misses ( L~ h) by A22, A25, A13, Th49;

      

       A30: 2 <= ( len h) by TOPREAL1:def 8;

      1 <= i1 by A20, FINSEQ_3: 25;

      then

       A31: ( len M) = ((( len z) -' i1) + 1) by A22, JORDAN4: 9;

      then

       A32: (M /. ( len M)) in ( L~ M) by A24, JORDAN3: 1;

      

       A33: (z /. 1) = (z /. ( len z)) by FINSEQ_6:def 1;

      then

       A34: (M /. 1) = (z /. 1) by A20, A27, Th8;

      per cases ;

        suppose that

         A35: ( NW-corner ( L~ z)) = ( N-min ( L~ z)) and

         A36: ( NE-corner ( L~ z)) = ( N-max ( L~ z));

        

         A37: ((M /. ( len M)) `1 ) = ( E-bound ( L~ z)) by A28, A36, EUCLID: 52;

        (M /. 1) = (z /. ( len z)) by A20, A27, Th8;

        then

         A38: ((M /. 1) `1 ) = ( W-bound ( L~ z)) by A1, A33, A35, EUCLID: 52;

        M is_in_the_area_of z by A20, A27, Th21, Th22;

        then M is_a_h.c._for z by A38, A37;

        hence contradiction by A18, A29, A31, A24, A30, Th29;

      end;

        suppose that

         A39: ( NW-corner ( L~ z)) = ( N-min ( L~ z)) and

         A40: ( NE-corner ( L~ z)) <> ( N-max ( L~ z));

        reconsider g = (M ^ <*( NE-corner ( L~ z))*>) as S-Sequence_in_R2 by A20, A21, A27, A40, Th62;

        

         A41: ( len g) >= 2 & ( L~ g) = (( L~ M) \/ ( LSeg ((M /. ( len M)),( NE-corner ( L~ z))))) by SPPOL_2: 19, TOPREAL1:def 8;

        ( len g) = (( len M) + ( len <*( NE-corner ( L~ z))*>)) by FINSEQ_1: 22

        .= (( len M) + 1) by FINSEQ_1: 39;

        then (g /. ( len g)) = ( NE-corner ( L~ z)) by FINSEQ_4: 67;

        then

         A42: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

        M is_in_the_area_of z & <*( NE-corner ( L~ z))*> is_in_the_area_of z by A20, A27, Th21, Th22, Th25;

        then

         A43: g is_in_the_area_of z by Th24;

        (( LSeg ((M /. ( len M)),( NE-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. ( len M)),( NE-corner ( L~ z)))) /\ ( L~ z)) by A9, A6, A14, JORDAN4: 35, XBOOLE_1: 26;

        then

         A44: (( LSeg ((M /. ( len M)),( NE-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. ( len M))} by A28, PSCOMP_1: 43;

        (g /. 1) = (M /. 1) by A26, FINSEQ_4: 68

        .= (z /. 1) by A20, A27, A33, Th8;

        then ((g /. 1) `1 ) = ( W-bound ( L~ z)) by A1, A39, EUCLID: 52;

        then g is_a_h.c._for z by A43, A42;

        hence contradiction by A18, A29, A32, A30, A41, A44, Th29, ZFMISC_1: 125;

      end;

        suppose that

         A45: ( NW-corner ( L~ z)) <> ( N-min ( L~ z)) and

         A46: ( NE-corner ( L~ z)) = ( N-max ( L~ z));

        reconsider g = ( <*( NW-corner ( L~ z))*> ^ M) as S-Sequence_in_R2 by A1, A20, A27, A33, A45, Th66;

        ( len M) in ( dom M) & ( len g) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22, FINSEQ_5: 6;

        

        then (g /. ( len g)) = (M /. ( len M)) by FINSEQ_4: 69

        .= (z /. i1) by A20, A27, Th9

        .= ( N-max ( L~ z)) by A19, FINSEQ_5: 38;

        then

         A47: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by A46, EUCLID: 52;

        

         A48: ( len g) >= 2 & ( L~ g) = (( L~ M) \/ ( LSeg (( NW-corner ( L~ z)),(M /. 1)))) by SPPOL_2: 20, TOPREAL1:def 8;

        (g /. 1) = ( NW-corner ( L~ z)) by FINSEQ_5: 15;

        then

         A49: ((g /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

        (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ z)) by A9, A6, A14, JORDAN4: 35, XBOOLE_1: 26;

        then

         A50: (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. 1)} by A1, A34, PSCOMP_1: 43;

        

         A51: (M /. 1) in ( L~ M) by A31, A24, JORDAN3: 1;

        M is_in_the_area_of z & <*( NW-corner ( L~ z))*> is_in_the_area_of z by A20, A27, Th21, Th22, Th26;

        then g is_in_the_area_of z by Th24;

        then g is_a_h.c._for z by A49, A47;

        hence contradiction by A18, A29, A30, A48, A50, A51, Th29, ZFMISC_1: 125;

      end;

        suppose that

         A52: ( NW-corner ( L~ z)) <> ( N-min ( L~ z)) & ( NE-corner ( L~ z)) <> ( N-max ( L~ z));

        set K = ( <*( NW-corner ( L~ z))*> ^ M);

        reconsider g = (K ^ <*( NE-corner ( L~ z))*>) as S-Sequence_in_R2 by A1, A20, A21, A27, A33, A52, Lm1;

        1 in ( dom ( <*( NW-corner ( L~ z))*> ^ M)) by FINSEQ_5: 6;

        

        then (g /. 1) = (( <*( NW-corner ( L~ z))*> ^ M) /. 1) by FINSEQ_4: 68

        .= ( NW-corner ( L~ z)) by FINSEQ_5: 15;

        then

         A53: ((g /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

        ( len g) = (( len ( <*( NW-corner ( L~ z))*> ^ M)) + ( len <*( NE-corner ( L~ z))*>)) by FINSEQ_1: 22

        .= (( len ( <*( NW-corner ( L~ z))*> ^ M)) + 1) by FINSEQ_1: 39;

        then (g /. ( len g)) = ( NE-corner ( L~ z)) by FINSEQ_4: 67;

        then

         A54: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

        M is_in_the_area_of z & <*( NW-corner ( L~ z))*> is_in_the_area_of z by A20, A27, Th21, Th22, Th26;

        then

         A55: ( <*( NW-corner ( L~ z))*> ^ M) is_in_the_area_of z by Th24;

         <*( NE-corner ( L~ z))*> is_in_the_area_of z by Th25;

        then g is_in_the_area_of z by A55, Th24;

        then

         A56: g is_a_h.c._for z by A53, A54;

        ( len K) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22;

        then ( len K) >= ( len M) by NAT_1: 11;

        then ( len K) >= 2 by A31, A24, XXREAL_0: 2;

        then

         A57: (K /. ( len K)) in ( L~ K) by JORDAN3: 1;

        (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ z)) by A9, A6, A14, JORDAN4: 35, XBOOLE_1: 26;

        then

         A58: (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. 1)} by A1, A34, PSCOMP_1: 43;

        ( L~ K) = (( L~ M) \/ ( LSeg (( NW-corner ( L~ z)),(M /. 1)))) & (M /. 1) in ( L~ M) by A31, A24, JORDAN3: 1, SPPOL_2: 20;

        then

         A59: ( L~ K) misses ( L~ h) by A29, A58, ZFMISC_1: 125;

        ( len M) in ( dom M) & ( len K) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22, FINSEQ_5: 6;

        

        then

         A60: (K /. ( len K)) = (M /. ( len M)) by FINSEQ_4: 69

        .= (z /. i1) by A20, A27, Th9

        .= ( N-max ( L~ z)) by A19, FINSEQ_5: 38;

        (( LSeg ((K /. ( len K)),( NE-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((K /. ( len K)),( NE-corner ( L~ z)))) /\ ( L~ z)) by A9, A6, A14, JORDAN4: 35, XBOOLE_1: 26;

        then

         A61: (( LSeg ((K /. ( len K)),( NE-corner ( L~ z)))) /\ ( L~ h)) c= {(K /. ( len K))} by A60, PSCOMP_1: 43;

        ( len g) >= 2 & ( L~ g) = (( L~ K) \/ ( LSeg ((K /. ( len K)),( NE-corner ( L~ z))))) by SPPOL_2: 19, TOPREAL1:def 8;

        hence contradiction by A18, A30, A56, A59, A57, A61, Th29, ZFMISC_1: 125;

      end;

    end;

    

     Lm6: (z /. 1) = ( N-min ( L~ z)) implies (( N-max ( L~ z)) .. z) < (( S-min ( L~ z)) .. z)

    proof

      set i1 = (( N-max ( L~ z)) .. z), i2 = (( S-min ( L~ z)) .. z);

      assume that

       A1: (z /. 1) = ( N-min ( L~ z)) and

       A2: i1 >= i2;

      

       A3: ( N-min ( L~ z)) <> ( N-max ( L~ z)) by Th52;

      (z /. 2) in ( N-most ( L~ z)) by A1, Th30;

      

      then

       A4: ((z /. 2) `2 ) = (( N-min ( L~ z)) `2 ) by PSCOMP_1: 39

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

      

       A5: ( S-bound ( L~ z)) < ( N-bound ( L~ z)) by TOPREAL5: 16;

      

       A6: ( S-min ( L~ z)) in ( rng z) by Th41;

      then

       A7: i2 in ( dom z) by FINSEQ_4: 20;

      then

       A8: i2 <= ( len z) by FINSEQ_3: 25;

      

       A9: (z /. i2) = (z . i2) by A7, PARTFUN1:def 6

      .= ( S-min ( L~ z)) by A6, FINSEQ_4: 19;

      then

       A10: ((z /. i2) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      

       A11: 1 <= i2 by A7, FINSEQ_3: 25;

      

       A12: i2 <> 0 by A7, FINSEQ_3: 25;

      ((z /. 1) `2 ) = ( N-bound ( L~ z)) by A1, EUCLID: 52;

      then i2 <> 0 & ... & i2 <> 2 by A4, A12, A10, A5;

      then

       A13: i2 > 2;

      then

      reconsider h = ( mid (z,i2,2)) as S-Sequence_in_R2 by A8, Th37;

      

       A14: 2 <= ( len z) by NAT_D: 60;

      then

       A15: 2 in ( dom z) by FINSEQ_3: 25;

      then (h /. 1) = ( S-min ( L~ z)) by A7, A9, Th8;

      then

       A16: ((h /. 1) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      h is_in_the_area_of z & (h /. ( len h)) = (z /. 2) by A7, A15, Th9, Th21, Th22;

      then

       A17: ( len h) >= 2 & h is_a_v.c._for z by A4, A16, TOPREAL1:def 8;

      

       A18: ( N-max ( L~ z)) in ( rng z) by Th40;

      then

       A19: i1 in ( dom z) by FINSEQ_4: 20;

      

      then

       A20: (z /. i1) = (z . i1) by PARTFUN1:def 6

      .= ( N-max ( L~ z)) by A18, FINSEQ_4: 19;

      

       A21: i1 <= ( len z) by A19, FINSEQ_3: 25;

      (z /. ( len z)) = ( N-min ( L~ z)) by A1, FINSEQ_6:def 1;

      then

       A22: i1 < ( len z) by A21, A20, A3, XXREAL_0: 1;

      then (i1 + 1) <= ( len z) by NAT_1: 13;

      then (( len z) - i1) >= 1 by XREAL_1: 19;

      then (( len z) -' i1) >= 1 by NAT_D: 39;

      then

       A23: ((( len z) -' i1) + 1) >= (1 + 1) by XREAL_1: 6;

      (( N-max ( L~ z)) `2 ) = ( N-bound ( L~ z)) & (( S-min ( L~ z)) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      then (z /. i1) <> (z /. i2) by A9, A20, TOPREAL5: 16;

      then

       A24: i1 > i2 by A2, XXREAL_0: 1;

      then i1 > 1 by A11, XXREAL_0: 2;

      then

      reconsider M = ( mid (z,( len z),i1)) as S-Sequence_in_R2 by A22, Th37;

      

       A25: 1 in ( dom M) by FINSEQ_5: 6;

      

       A26: ( len z) in ( dom z) by FINSEQ_5: 6;

      

      then

       A27: (M /. ( len M)) = (z /. i1) by A19, Th9

      .= ( N-max ( L~ z)) by A18, FINSEQ_5: 38;

      

       A28: ( L~ M) misses ( L~ h) by A21, A24, A13, Th49;

      1 <= i1 by A19, FINSEQ_3: 25;

      then

       A29: ( len M) = ((( len z) -' i1) + 1) by A21, JORDAN4: 9;

      then

       A30: (M /. ( len M)) in ( L~ M) by A23, JORDAN3: 1;

      

       A31: (z /. 1) = (z /. ( len z)) by FINSEQ_6:def 1;

      then

       A32: (M /. 1) = (z /. 1) by A19, A26, Th8;

      per cases ;

        suppose that

         A33: ( NW-corner ( L~ z)) = ( N-min ( L~ z)) and

         A34: ( NE-corner ( L~ z)) = ( N-max ( L~ z));

        

         A35: ((M /. ( len M)) `1 ) = ( E-bound ( L~ z)) by A27, A34, EUCLID: 52;

        (M /. 1) = (z /. ( len z)) by A19, A26, Th8;

        then

         A36: ((M /. 1) `1 ) = ( W-bound ( L~ z)) by A1, A31, A33, EUCLID: 52;

        M is_in_the_area_of z by A19, A26, Th21, Th22;

        then M is_a_h.c._for z by A36, A35;

        hence contradiction by A17, A28, A29, A23, Th29;

      end;

        suppose that

         A37: ( NW-corner ( L~ z)) = ( N-min ( L~ z)) and

         A38: ( NE-corner ( L~ z)) <> ( N-max ( L~ z));

        reconsider g = (M ^ <*( NE-corner ( L~ z))*>) as S-Sequence_in_R2 by A19, A20, A26, A38, Th62;

        

         A39: ( len g) >= 2 & ( L~ g) = (( L~ M) \/ ( LSeg ((M /. ( len M)),( NE-corner ( L~ z))))) by SPPOL_2: 19, TOPREAL1:def 8;

        ( len g) = (( len M) + ( len <*( NE-corner ( L~ z))*>)) by FINSEQ_1: 22

        .= (( len M) + 1) by FINSEQ_1: 39;

        then (g /. ( len g)) = ( NE-corner ( L~ z)) by FINSEQ_4: 67;

        then

         A40: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

        M is_in_the_area_of z & <*( NE-corner ( L~ z))*> is_in_the_area_of z by A19, A26, Th21, Th22, Th25;

        then

         A41: g is_in_the_area_of z by Th24;

        (( LSeg ((M /. ( len M)),( NE-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. ( len M)),( NE-corner ( L~ z)))) /\ ( L~ z)) by A11, A8, A14, JORDAN4: 35, XBOOLE_1: 26;

        then

         A42: (( LSeg ((M /. ( len M)),( NE-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. ( len M))} by A27, PSCOMP_1: 43;

        (g /. 1) = (M /. 1) by A25, FINSEQ_4: 68

        .= (z /. 1) by A19, A26, A31, Th8;

        then ((g /. 1) `1 ) = ( W-bound ( L~ z)) by A1, A37, EUCLID: 52;

        then g is_a_h.c._for z by A41, A40;

        hence contradiction by A17, A28, A30, A39, A42, Th29, ZFMISC_1: 125;

      end;

        suppose that

         A43: ( NW-corner ( L~ z)) <> ( N-min ( L~ z)) and

         A44: ( NE-corner ( L~ z)) = ( N-max ( L~ z));

        reconsider g = ( <*( NW-corner ( L~ z))*> ^ M) as S-Sequence_in_R2 by A1, A19, A26, A31, A43, Th66;

        ( len M) in ( dom M) & ( len g) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22, FINSEQ_5: 6;

        

        then (g /. ( len g)) = (M /. ( len M)) by FINSEQ_4: 69

        .= (z /. i1) by A19, A26, Th9

        .= ( N-max ( L~ z)) by A18, FINSEQ_5: 38;

        then

         A45: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by A44, EUCLID: 52;

        

         A46: ( len g) >= 2 & ( L~ g) = (( L~ M) \/ ( LSeg (( NW-corner ( L~ z)),(M /. 1)))) by SPPOL_2: 20, TOPREAL1:def 8;

        (g /. 1) = ( NW-corner ( L~ z)) by FINSEQ_5: 15;

        then

         A47: ((g /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

        (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ z)) by A11, A8, A14, JORDAN4: 35, XBOOLE_1: 26;

        then

         A48: (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. 1)} by A1, A32, PSCOMP_1: 43;

        

         A49: (M /. 1) in ( L~ M) by A29, A23, JORDAN3: 1;

        M is_in_the_area_of z & <*( NW-corner ( L~ z))*> is_in_the_area_of z by A19, A26, Th21, Th22, Th26;

        then g is_in_the_area_of z by Th24;

        then g is_a_h.c._for z by A47, A45;

        hence contradiction by A17, A28, A46, A48, A49, Th29, ZFMISC_1: 125;

      end;

        suppose that

         A50: ( NW-corner ( L~ z)) <> ( N-min ( L~ z)) & ( NE-corner ( L~ z)) <> ( N-max ( L~ z));

        set K = ( <*( NW-corner ( L~ z))*> ^ M);

        reconsider g = (K ^ <*( NE-corner ( L~ z))*>) as S-Sequence_in_R2 by A1, A19, A20, A26, A31, A50, Lm1;

        1 in ( dom ( <*( NW-corner ( L~ z))*> ^ M)) by FINSEQ_5: 6;

        

        then (g /. 1) = (( <*( NW-corner ( L~ z))*> ^ M) /. 1) by FINSEQ_4: 68

        .= ( NW-corner ( L~ z)) by FINSEQ_5: 15;

        then

         A51: ((g /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

        ( len g) = (( len ( <*( NW-corner ( L~ z))*> ^ M)) + ( len <*( NE-corner ( L~ z))*>)) by FINSEQ_1: 22

        .= (( len ( <*( NW-corner ( L~ z))*> ^ M)) + 1) by FINSEQ_1: 39;

        then (g /. ( len g)) = ( NE-corner ( L~ z)) by FINSEQ_4: 67;

        then

         A52: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

        M is_in_the_area_of z & <*( NW-corner ( L~ z))*> is_in_the_area_of z by A19, A26, Th21, Th22, Th26;

        then

         A53: ( <*( NW-corner ( L~ z))*> ^ M) is_in_the_area_of z by Th24;

         <*( NE-corner ( L~ z))*> is_in_the_area_of z by Th25;

        then g is_in_the_area_of z by A53, Th24;

        then

         A54: g is_a_h.c._for z by A51, A52;

        ( len K) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22;

        then ( len K) >= ( len M) by NAT_1: 11;

        then ( len K) >= 2 by A29, A23, XXREAL_0: 2;

        then

         A55: (K /. ( len K)) in ( L~ K) by JORDAN3: 1;

        (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ z)) by A11, A8, A14, JORDAN4: 35, XBOOLE_1: 26;

        then

         A56: (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. 1)} by A1, A32, PSCOMP_1: 43;

        ( L~ K) = (( L~ M) \/ ( LSeg (( NW-corner ( L~ z)),(M /. 1)))) & (M /. 1) in ( L~ M) by A29, A23, JORDAN3: 1, SPPOL_2: 20;

        then

         A57: ( L~ K) misses ( L~ h) by A28, A56, ZFMISC_1: 125;

        ( len M) in ( dom M) & ( len K) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22, FINSEQ_5: 6;

        

        then

         A58: (K /. ( len K)) = (M /. ( len M)) by FINSEQ_4: 69

        .= (z /. i1) by A19, A26, Th9

        .= ( N-max ( L~ z)) by A18, FINSEQ_5: 38;

        (( LSeg ((K /. ( len K)),( NE-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((K /. ( len K)),( NE-corner ( L~ z)))) /\ ( L~ z)) by A11, A8, A14, JORDAN4: 35, XBOOLE_1: 26;

        then

         A59: (( LSeg ((K /. ( len K)),( NE-corner ( L~ z)))) /\ ( L~ h)) c= {(K /. ( len K))} by A58, PSCOMP_1: 43;

        ( len g) >= 2 & ( L~ g) = (( L~ K) \/ ( LSeg ((K /. ( len K)),( NE-corner ( L~ z))))) by SPPOL_2: 19, TOPREAL1:def 8;

        hence contradiction by A17, A54, A57, A55, A59, Th29, ZFMISC_1: 125;

      end;

    end;

    theorem :: SPRECT_2:70

    (z /. 1) = ( N-min ( L~ z)) & ( N-max ( L~ z)) <> ( E-max ( L~ z)) implies (( N-max ( L~ z)) .. z) < (( E-max ( L~ z)) .. z)

    proof

      set i1 = (( N-max ( L~ z)) .. z), i2 = (( E-max ( L~ z)) .. z), j = (( S-max ( L~ z)) .. z);

      assume that

       A1: (z /. 1) = ( N-min ( L~ z)) and

       A2: ( N-max ( L~ z)) <> ( E-max ( L~ z)) & i1 >= i2;

      (( N-min ( L~ z)) .. z) = 1 by A1, FINSEQ_6: 43;

      then

       A3: 1 < i2 by A1, Lm4;

      (( N-min ( L~ z)) `2 ) = ( N-bound ( L~ z)) & (( S-max ( L~ z)) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      then

       A4: ( N-min ( L~ z)) <> ( S-max ( L~ z)) by TOPREAL5: 16;

      

       A5: ( S-max ( L~ z)) in ( rng z) by Th42;

      then

       A6: j in ( dom z) by FINSEQ_4: 20;

      

      then

       A7: (z /. j) = (z . j) by PARTFUN1:def 6

      .= ( S-max ( L~ z)) by A5, FINSEQ_4: 19;

      

       A8: j <= ( len z) by A6, FINSEQ_3: 25;

      (z /. ( len z)) = (z /. 1) by FINSEQ_6:def 1;

      then

       A9: j < ( len z) by A1, A8, A7, A4, XXREAL_0: 1;

      

       A10: ( N-max ( L~ z)) in ( rng z) by Th40;

      then

       A11: i1 in ( dom z) by FINSEQ_4: 20;

      then

       A12: 1 <= i1 by FINSEQ_3: 25;

      

       A13: (z /. i1) = (z . i1) by A11, PARTFUN1:def 6

      .= ( N-max ( L~ z)) by A10, FINSEQ_4: 19;

      

       A14: j > i1 by A1, Lm5;

      then

      reconsider h = ( mid (z,j,i1)) as S-Sequence_in_R2 by A12, A9, Th37;

      (h /. 1) = ( S-max ( L~ z)) by A11, A6, A7, Th8;

      then

       A15: ((h /. 1) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      (h /. ( len h)) = (z /. i1) by A11, A6, Th9;

      then

       A16: ((h /. ( len h)) `2 ) = ( N-bound ( L~ z)) by A13, EUCLID: 52;

      h is_in_the_area_of z by A11, A6, Th21, Th22;

      then

       A17: h is_a_v.c._for z by A15, A16;

      

       A18: 1 <= j by A6, FINSEQ_3: 25;

      

       A19: i1 <= ( len z) by A11, FINSEQ_3: 25;

      

       A20: ( E-max ( L~ z)) in ( rng z) by Th46;

      then

       A21: i2 in ( dom z) by FINSEQ_4: 20;

      then

       A22: 1 <= i2 & i2 <= ( len z) by FINSEQ_3: 25;

      (z /. i2) = (z . i2) by A21, PARTFUN1:def 6

      .= ( E-max ( L~ z)) by A20, FINSEQ_4: 19;

      then

       A23: i1 > i2 by A2, A13, XXREAL_0: 1;

      then i2 < ( len z) by A19, XXREAL_0: 2;

      then

      reconsider M = ( mid (z,1,i2)) as S-Sequence_in_R2 by A3, Th38;

      

       A24: ( len M) >= 2 by TOPREAL1:def 8;

      

       A25: 1 in ( dom z) by FINSEQ_5: 6;

      

      then

       A26: (M /. ( len M)) = (z /. i2) by A21, Th9

      .= ( E-max ( L~ z)) by A20, FINSEQ_5: 38;

      

       A27: ( len h) >= 2 & ( L~ M) misses ( L~ h) by A14, A9, A3, A23, Th48, TOPREAL1:def 8;

      per cases ;

        suppose

         A28: ( NW-corner ( L~ z)) = ( N-min ( L~ z));

        (M /. 1) = (z /. 1) by A25, A21, Th8;

        then

         A29: ((M /. 1) `1 ) = ( W-bound ( L~ z)) by A1, A28, EUCLID: 52;

        M is_in_the_area_of z & ((M /. ( len M)) `1 ) = ( E-bound ( L~ z)) by A25, A21, A26, Th21, Th22, EUCLID: 52;

        then M is_a_h.c._for z by A29;

        hence contradiction by A17, A24, A27, Th29;

      end;

        suppose ( NW-corner ( L~ z)) <> ( N-min ( L~ z));

        then

        reconsider g = ( <*( NW-corner ( L~ z))*> ^ M) as S-Sequence_in_R2 by A1, A25, A21, Th66;

        

         A30: ( len g) >= 2 & ( L~ g) = (( L~ M) \/ ( LSeg (( NW-corner ( L~ z)),(M /. 1)))) by SPPOL_2: 20, TOPREAL1:def 8;

        (g /. 1) = ( NW-corner ( L~ z)) by FINSEQ_5: 15;

        then

         A31: ((g /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

        ( len M) = ((i2 -' 1) + 1) by A22, JORDAN4: 8

        .= i2 by A3, XREAL_1: 235;

        then ( len M) >= (1 + 1) by A3, NAT_1: 13;

        then

         A32: (M /. 1) in ( L~ M) by JORDAN3: 1;

        ( len M) in ( dom M) & ( len g) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22, FINSEQ_5: 6;

        

        then (g /. ( len g)) = (M /. ( len M)) by FINSEQ_4: 69

        .= (z /. i2) by A25, A21, Th9

        .= ( E-max ( L~ z)) by A20, FINSEQ_5: 38;

        then

         A33: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

        (M /. 1) = (z /. 1) & (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ z)) by A25, A12, A19, A18, A8, A21, Th8, JORDAN4: 35, XBOOLE_1: 26;

        then

         A34: (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. 1)} by A1, PSCOMP_1: 43;

        M is_in_the_area_of z & <*( NW-corner ( L~ z))*> is_in_the_area_of z by A25, A21, Th21, Th22, Th26;

        then g is_in_the_area_of z by Th24;

        then g is_a_h.c._for z by A31, A33;

        hence contradiction by A17, A27, A30, A34, A32, Th29, ZFMISC_1: 125;

      end;

    end;

    

     Lm7: (z /. 1) = ( N-min ( L~ z)) implies (( E-max ( L~ z)) .. z) < (( S-max ( L~ z)) .. z)

    proof

      set i1 = (( E-max ( L~ z)) .. z), i2 = (( S-max ( L~ z)) .. z);

      assume that

       A1: (z /. 1) = ( N-min ( L~ z)) and

       A2: i1 >= i2;

      

       A3: (( N-min ( L~ z)) `1 ) < (( N-max ( L~ z)) `1 ) by Th51;

      (z /. 2) in ( N-most ( L~ z)) by A1, Th30;

      

      then

       A4: ((z /. 2) `2 ) = (( N-min ( L~ z)) `2 ) by PSCOMP_1: 39

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

      ( E-min ( L~ z)) in ( L~ z) by SPRECT_1: 14;

      then

       A5: ( S-bound ( L~ z)) <= (( E-min ( L~ z)) `2 ) by PSCOMP_1: 24;

      

       A6: ( S-bound ( L~ z)) < ( N-bound ( L~ z)) by TOPREAL5: 16;

      

       A7: ( S-max ( L~ z)) in ( rng z) by Th42;

      then

       A8: i2 in ( dom z) by FINSEQ_4: 20;

      then

       A9: i2 <= ( len z) by FINSEQ_3: 25;

      

       A10: i2 <> 0 by A8, FINSEQ_3: 25;

      

       A11: (z /. i2) = (z . i2) by A8, PARTFUN1:def 6

      .= ( S-max ( L~ z)) by A7, FINSEQ_4: 19;

      then

       A12: ((z /. i2) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      

       A13: 1 <= i2 by A8, FINSEQ_3: 25;

      ((z /. 1) `2 ) = ( N-bound ( L~ z)) by A1, EUCLID: 52;

      then i2 <> 0 & ... & i2 <> 2 by A4, A10, A12, A6;

      then

       A14: i2 > 2;

      then

      reconsider h = ( mid (z,i2,2)) as S-Sequence_in_R2 by A9, Th37;

      

       A15: 2 <= ( len z) by NAT_D: 60;

      then

       A16: 2 in ( dom z) by FINSEQ_3: 25;

      then (h /. 1) = ( S-max ( L~ z)) by A8, A11, Th8;

      then

       A17: ((h /. 1) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      h is_in_the_area_of z & (h /. ( len h)) = (z /. 2) by A8, A16, Th9, Th21, Th22;

      then

       A18: ( len h) >= 2 & h is_a_v.c._for z by A4, A17, TOPREAL1:def 8;

      ( N-max ( L~ z)) in ( L~ z) by SPRECT_1: 11;

      then

       A19: (( N-max ( L~ z)) `1 ) <= ( E-bound ( L~ z)) by PSCOMP_1: 24;

      

       A20: ( E-max ( L~ z)) in ( rng z) by Th46;

      then

       A21: i1 in ( dom z) by FINSEQ_4: 20;

      

      then

       A22: (z /. i1) = (z . i1) by PARTFUN1:def 6

      .= ( E-max ( L~ z)) by A20, FINSEQ_4: 19;

      

       A23: i1 <= ( len z) by A21, FINSEQ_3: 25;

      (z /. ( len z)) = ( N-min ( L~ z)) by A1, FINSEQ_6:def 1;

      then i1 <> ( len z) by A22, A3, A19, EUCLID: 52;

      then

       A24: i1 < ( len z) by A23, XXREAL_0: 1;

      then (i1 + 1) <= ( len z) by NAT_1: 13;

      then (( len z) - i1) >= 1 by XREAL_1: 19;

      then (( len z) -' i1) >= 1 by NAT_D: 39;

      then

       A25: ((( len z) -' i1) + 1) >= (1 + 1) by XREAL_1: 6;

      (( E-min ( L~ z)) `2 ) < (( E-max ( L~ z)) `2 ) by Th53;

      then ( E-max ( L~ z)) <> ( S-max ( L~ z)) by A5, EUCLID: 52;

      then

       A26: i1 > i2 by A2, A11, A22, XXREAL_0: 1;

      then i1 > 1 by A13, XXREAL_0: 2;

      then

      reconsider M = ( mid (z,( len z),i1)) as S-Sequence_in_R2 by A24, Th37;

      

       A27: ( len M) >= 2 by TOPREAL1:def 8;

      1 <= i1 by A21, FINSEQ_3: 25;

      then

       A28: ( len M) = ((( len z) -' i1) + 1) by A23, JORDAN4: 9;

      

       A29: ( len z) in ( dom z) by FINSEQ_5: 6;

      

      then

       A30: (M /. ( len M)) = (z /. i1) by A21, Th9

      .= ( E-max ( L~ z)) by A20, FINSEQ_5: 38;

      

       A31: ( L~ M) misses ( L~ h) by A23, A26, A14, Th49;

      

       A32: (z /. 1) = (z /. ( len z)) by FINSEQ_6:def 1;

      then

       A33: (M /. 1) = (z /. 1) by A21, A29, Th8;

      per cases ;

        suppose that

         A34: ( NW-corner ( L~ z)) = ( N-min ( L~ z));

        (M /. 1) = (z /. ( len z)) by A21, A29, Th8;

        then

         A35: ((M /. 1) `1 ) = ( W-bound ( L~ z)) by A1, A32, A34, EUCLID: 52;

        M is_in_the_area_of z & ((M /. ( len M)) `1 ) = ( E-bound ( L~ z)) by A21, A29, A30, Th21, Th22, EUCLID: 52;

        then M is_a_h.c._for z by A35;

        hence contradiction by A18, A27, A31, Th29;

      end;

        suppose ( NW-corner ( L~ z)) <> ( N-min ( L~ z));

        then

        reconsider g = ( <*( NW-corner ( L~ z))*> ^ M) as S-Sequence_in_R2 by A1, A21, A29, A32, Th66;

        

         A36: ( len g) >= 2 & ( L~ g) = (( L~ M) \/ ( LSeg (( NW-corner ( L~ z)),(M /. 1)))) by SPPOL_2: 20, TOPREAL1:def 8;

        (g /. 1) = ( NW-corner ( L~ z)) by FINSEQ_5: 15;

        then

         A37: ((g /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

        (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ z)) by A13, A9, A15, JORDAN4: 35, XBOOLE_1: 26;

        then

         A38: (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. 1)} by A1, A33, PSCOMP_1: 43;

        ( len M) in ( dom M) & ( len g) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22, FINSEQ_5: 6;

        

        then (g /. ( len g)) = (M /. ( len M)) by FINSEQ_4: 69

        .= (z /. i1) by A21, A29, Th9

        .= ( E-max ( L~ z)) by A20, FINSEQ_5: 38;

        then

         A39: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

        

         A40: (M /. 1) in ( L~ M) by A28, A25, JORDAN3: 1;

        M is_in_the_area_of z & <*( NW-corner ( L~ z))*> is_in_the_area_of z by A21, A29, Th21, Th22, Th26;

        then g is_in_the_area_of z by Th24;

        then g is_a_h.c._for z by A37, A39;

        hence contradiction by A18, A31, A36, A38, A40, Th29, ZFMISC_1: 125;

      end;

    end;

    

     Lm8: (( LSeg (( N-min ( L~ f)),( NW-corner ( L~ f)))) /\ ( LSeg (( NE-corner ( L~ f)),( E-max ( L~ f))))) = {}

    proof

      

       A1: (( NE-corner ( L~ f)) `1 ) = ( E-bound ( L~ f)) & (( E-max ( L~ f)) `1 ) = ( E-bound ( L~ f)) by EUCLID: 52;

      assume (( LSeg (( N-min ( L~ f)),( NW-corner ( L~ f)))) /\ ( LSeg (( NE-corner ( L~ f)),( E-max ( L~ f))))) <> {} ;

      then

      consider x be object such that

       A2: x in (( LSeg (( N-min ( L~ f)),( NW-corner ( L~ f)))) /\ ( LSeg (( NE-corner ( L~ f)),( E-max ( L~ f))))) by XBOOLE_0:def 1;

      reconsider p = x as Point of ( TOP-REAL 2) by A2;

      p in ( LSeg (( NE-corner ( L~ f)),( E-max ( L~ f)))) by A2, XBOOLE_0:def 4;

      then ( E-bound ( L~ f)) <= (p `1 ) & (p `1 ) <= ( E-bound ( L~ f)) by A1, TOPREAL1: 3;

      then

       A3: (p `1 ) = ( E-bound ( L~ f)) by XXREAL_0: 1;

      

       A4: (( NW-corner ( L~ f)) `1 ) <= (( N-min ( L~ f)) `1 ) by PSCOMP_1: 38;

      (( N-max ( L~ f)) `1 ) <= (( NE-corner ( L~ f)) `1 ) by PSCOMP_1: 38;

      then

       A5: (( N-min ( L~ f)) `1 ) < (( NE-corner ( L~ f)) `1 ) by Th51, XXREAL_0: 2;

      x in ( LSeg (( N-min ( L~ f)),( NW-corner ( L~ f)))) by A2, XBOOLE_0:def 4;

      then (p `1 ) <= (( N-min ( L~ f)) `1 ) by A4, TOPREAL1: 3;

      hence contradiction by A3, A5, EUCLID: 52;

    end;

    theorem :: SPRECT_2:71

    (z /. 1) = ( N-min ( L~ z)) implies (( E-max ( L~ z)) .. z) < (( E-min ( L~ z)) .. z)

    proof

      set i1 = (( E-max ( L~ z)) .. z), i2 = (( E-min ( L~ z)) .. z), j = (( S-max ( L~ z)) .. z);

      assume that

       A1: (z /. 1) = ( N-min ( L~ z)) and

       A2: i1 >= i2;

      

       A3: i1 < j by A1, Lm7;

      

       A4: ( E-min ( L~ z)) in ( rng z) by Th45;

      then

       A5: i2 in ( dom z) by FINSEQ_4: 20;

      then

       A6: 1 <= i2 by FINSEQ_3: 25;

      

       A7: (z /. i2) = (z . i2) by A5, PARTFUN1:def 6

      .= ( E-min ( L~ z)) by A4, FINSEQ_4: 19;

      ( N-max ( L~ z)) in ( L~ z) by SPRECT_1: 11;

      then (( N-max ( L~ z)) `1 ) <= ( E-bound ( L~ z)) by PSCOMP_1: 24;

      then (( N-min ( L~ z)) `1 ) < ( E-bound ( L~ z)) by Th51, XXREAL_0: 2;

      then (( N-min ( L~ z)) `1 ) < (( E-min ( L~ z)) `1 ) by EUCLID: 52;

      then

       A8: i2 > 1 by A1, A6, A7, XXREAL_0: 1;

      

       A9: i2 <= ( len z) by A5, FINSEQ_3: 25;

      then

       A10: 1 <= ( len z) by A6, XXREAL_0: 2;

      

       A11: (( S-max ( L~ z)) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      

       A12: ( S-bound ( L~ z)) < ( N-bound ( L~ z)) & (( N-min ( L~ z)) `2 ) = ( N-bound ( L~ z)) by EUCLID: 52, TOPREAL5: 16;

      

       A13: ( S-max ( L~ z)) in ( rng z) by Th42;

      then

       A14: j in ( dom z) by FINSEQ_4: 20;

      then

       A15: j <= ( len z) by FINSEQ_3: 25;

      

       A16: 1 <= j by A14, FINSEQ_3: 25;

      

       A17: ( E-max ( L~ z)) in ( rng z) by Th46;

      then

       A18: i1 in ( dom z) by FINSEQ_4: 20;

      

      then

       A19: (z /. i1) = (z . i1) by PARTFUN1:def 6

      .= ( E-max ( L~ z)) by A17, FINSEQ_4: 19;

      

       A20: 1 <= i1 by A18, FINSEQ_3: 25;

      

       A21: i1 <= ( len z) by A18, FINSEQ_3: 25;

      (( E-min ( L~ z)) `2 ) < (( E-max ( L~ z)) `2 ) by Th53;

      then

       A22: i1 > i2 by A2, A7, A19, XXREAL_0: 1;

      then i2 < ( len z) by A21, XXREAL_0: 2;

      then

      reconsider M = ( mid (z,1,i2)) as S-Sequence_in_R2 by A8, Th38;

      

       A23: 1 in ( dom z) by FINSEQ_5: 6;

      then

       A24: (M /. 1) = (z /. 1) by A5, Th8;

      i1 > 1 by A6, A22, XXREAL_0: 2;

      then

      reconsider h = ( mid (z,j,i1)) as S-Sequence_in_R2 by A15, A3, Th37;

      

       A25: (h /. ( len h)) = (z /. i1) by A18, A14, Th9;

      

       A26: (z /. j) = (z . j) by A14, PARTFUN1:def 6

      .= ( S-max ( L~ z)) by A13, FINSEQ_4: 19;

      then (h /. 1) = ( S-max ( L~ z)) by A18, A14, Th8;

      then

       A27: ((h /. 1) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      (M /. ( len M)) = (z /. i2) by A23, A5, Th9

      .= ( E-min ( L~ z)) by A4, FINSEQ_5: 38;

      then

       A28: ((M /. ( len M)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

      

       A29: M is_in_the_area_of z by A23, A5, Th21, Th22;

      ( len h) >= 1 by A18, A14, Th5;

      then ( len h) > 1 by A18, A14, A3, Th6, XXREAL_0: 1;

      then

       A30: ( len h) >= (1 + 1) by NAT_1: 13;

      ( len M) = ((i2 -' 1) + 1) by A6, A9, JORDAN4: 8

      .= i2 by A6, XREAL_1: 235;

      then

       A31: ( len M) >= (1 + 1) by A8, NAT_1: 13;

      

       A32: h is_in_the_area_of z by A18, A14, Th21, Th22;

      (z /. ( len z)) = ( N-min ( L~ z)) by A1, FINSEQ_6:def 1;

      then j < ( len z) by A15, A26, A12, A11, XXREAL_0: 1;

      then

       A33: ( L~ M) misses ( L~ h) by A6, A22, A3, Th48;

      per cases ;

        suppose that

         A34: ( NW-corner ( L~ z)) = ( N-min ( L~ z)) and

         A35: ( NE-corner ( L~ z)) = ( E-max ( L~ z));

        ((M /. 1) `1 ) = ( W-bound ( L~ z)) by A1, A24, A34, EUCLID: 52;

        then

         A36: M is_a_h.c._for z by A29, A28;

        ((h /. ( len h)) `2 ) = ( N-bound ( L~ z)) by A19, A25, A35, EUCLID: 52;

        then h is_a_v.c._for z by A32, A27;

        hence contradiction by A33, A31, A30, A36, Th29;

      end;

        suppose that

         A37: ( NW-corner ( L~ z)) <> ( N-min ( L~ z)) and

         A38: ( NE-corner ( L~ z)) = ( E-max ( L~ z));

        reconsider g = ( <*( NW-corner ( L~ z))*> ^ M) as S-Sequence_in_R2 by A1, A23, A5, A37, Th66;

        

         A39: 2 <= ( len g) & ( L~ g) = (( L~ M) \/ ( LSeg (( NW-corner ( L~ z)),(M /. 1)))) by SPPOL_2: 20, TOPREAL1:def 8;

        ((h /. ( len h)) `2 ) = ( N-bound ( L~ z)) by A19, A25, A38, EUCLID: 52;

        then

         A40: h is_a_v.c._for z by A32, A27;

        (g /. 1) = ( NW-corner ( L~ z)) by FINSEQ_5: 15;

        then

         A41: ((g /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

        ( len M) in ( dom M) & ( len g) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22, FINSEQ_5: 6;

        

        then (g /. ( len g)) = (M /. ( len M)) by FINSEQ_4: 69

        .= (z /. i2) by A23, A5, Th9

        .= ( E-min ( L~ z)) by A4, FINSEQ_5: 38;

        then

         A42: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

         <*( NW-corner ( L~ z))*> is_in_the_area_of z by Th26;

        then g is_in_the_area_of z by A29, Th24;

        then

         A43: g is_a_h.c._for z by A41, A42;

        (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ z)) by A20, A21, A16, A15, JORDAN4: 35, XBOOLE_1: 26;

        then

         A44: (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. 1)} by A1, A24, PSCOMP_1: 43;

        (M /. 1) in ( L~ M) by A31, JORDAN3: 1;

        hence contradiction by A33, A30, A40, A43, A39, A44, Th29, ZFMISC_1: 125;

      end;

        suppose that

         A45: ( NW-corner ( L~ z)) = ( N-min ( L~ z)) and

         A46: ( NE-corner ( L~ z)) <> ( E-max ( L~ z));

        reconsider N = (h ^ <*( NE-corner ( L~ z))*>) as S-Sequence_in_R2 by A18, A19, A14, A46, Th65;

        

         A47: ( len M) >= 2 & ( len N) >= 2 by TOPREAL1:def 8;

        (( LSeg ((h /. ( len h)),( NE-corner ( L~ z)))) /\ ( L~ M)) c= (( LSeg ((h /. ( len h)),( NE-corner ( L~ z)))) /\ ( L~ z)) by A6, A9, A10, JORDAN4: 35, XBOOLE_1: 26;

        then

         A48: (( LSeg ((h /. ( len h)),( NE-corner ( L~ z)))) /\ ( L~ M)) c= {(h /. ( len h))} by A19, A25, PSCOMP_1: 51;

        ( L~ N) = (( L~ h) \/ ( LSeg (( NE-corner ( L~ z)),(h /. ( len h))))) & (h /. ( len h)) in ( L~ h) by A30, JORDAN3: 1, SPPOL_2: 19;

        then

         A49: ( L~ M) misses ( L~ N) by A33, A48, ZFMISC_1: 125;

        ( len N) = (( len h) + ( len <*( NE-corner ( L~ z))*>)) by FINSEQ_1: 22

        .= (( len h) + 1) by FINSEQ_1: 39;

        then (N /. ( len N)) = ( NE-corner ( L~ z)) by FINSEQ_4: 67;

        then

         A50: ((N /. ( len N)) `2 ) = ( N-bound ( L~ z)) by EUCLID: 52;

        (M /. 1) = (z /. 1) by A23, A5, Th8;

        then ((M /. 1) `1 ) = ( W-bound ( L~ z)) by A1, A45, EUCLID: 52;

        then

         A51: M is_a_h.c._for z by A29, A28;

        1 in ( dom h) by FINSEQ_5: 6;

        then

         A52: ((N /. 1) `2 ) = ( S-bound ( L~ z)) by A27, FINSEQ_4: 68;

         <*( NE-corner ( L~ z))*> is_in_the_area_of z by Th25;

        then N is_in_the_area_of z by A32, Th24;

        then N is_a_v.c._for z by A52, A50;

        hence contradiction by A51, A47, A49, Th29;

      end;

        suppose that

         A53: ( NW-corner ( L~ z)) <> ( N-min ( L~ z)) and

         A54: ( NE-corner ( L~ z)) <> ( E-max ( L~ z));

        reconsider N = (h ^ <*( NE-corner ( L~ z))*>) as S-Sequence_in_R2 by A18, A19, A14, A54, Th65;

        reconsider g = ( <*( NW-corner ( L~ z))*> ^ M) as S-Sequence_in_R2 by A1, A23, A5, A53, Th66;

        

         A55: ( len g) >= 2 & ( len N) >= 2 by TOPREAL1:def 8;

        

         A56: ( L~ N) = (( L~ h) \/ ( LSeg (( NE-corner ( L~ z)),(h /. ( len h))))) by SPPOL_2: 19;

        (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( LSeg (( NE-corner ( L~ z)),(h /. ( len h))))) = {} by A1, A19, A25, A24, Lm8;

        

        then (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ N)) = ((( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) \/ {} ) by A56, XBOOLE_1: 23

        .= (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h));

        then (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ N)) c= (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ z)) by A20, A21, A16, A15, JORDAN4: 35, XBOOLE_1: 26;

        then

         A57: (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ N)) c= {(M /. 1)} by A1, A24, PSCOMP_1: 43;

        (g /. 1) = ( NW-corner ( L~ z)) by FINSEQ_5: 15;

        then

         A58: ((g /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

        ( len M) in ( dom M) & ( len g) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22, FINSEQ_5: 6;

        

        then (g /. ( len g)) = (M /. ( len M)) by FINSEQ_4: 69

        .= (z /. i2) by A23, A5, Th9

        .= ( E-min ( L~ z)) by A4, FINSEQ_5: 38;

        then

         A59: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

        ( len N) = (( len h) + ( len <*( NE-corner ( L~ z))*>)) by FINSEQ_1: 22

        .= (( len h) + 1) by FINSEQ_1: 39;

        then (N /. ( len N)) = ( NE-corner ( L~ z)) by FINSEQ_4: 67;

        then

         A60: ((N /. ( len N)) `2 ) = ( N-bound ( L~ z)) by EUCLID: 52;

        (( LSeg ((h /. ( len h)),( NE-corner ( L~ z)))) /\ ( L~ M)) c= (( LSeg ((h /. ( len h)),( NE-corner ( L~ z)))) /\ ( L~ z)) by A6, A9, A10, JORDAN4: 35, XBOOLE_1: 26;

        then

         A61: (( LSeg ((h /. ( len h)),( NE-corner ( L~ z)))) /\ ( L~ M)) c= {(h /. ( len h))} by A19, A25, PSCOMP_1: 51;

        (h /. ( len h)) in ( L~ h) by A30, JORDAN3: 1;

        then

         A62: ( L~ M) misses ( L~ N) by A33, A56, A61, ZFMISC_1: 125;

        1 in ( dom h) by FINSEQ_5: 6;

        then

         A63: ((N /. 1) `2 ) = ( S-bound ( L~ z)) by A27, FINSEQ_4: 68;

         <*( NE-corner ( L~ z))*> is_in_the_area_of z by Th25;

        then N is_in_the_area_of z by A32, Th24;

        then

         A64: N is_a_v.c._for z by A63, A60;

         <*( NW-corner ( L~ z))*> is_in_the_area_of z by Th26;

        then g is_in_the_area_of z by A29, Th24;

        then

         A65: g is_a_h.c._for z by A58, A59;

        ( L~ g) = (( L~ M) \/ ( LSeg (( NW-corner ( L~ z)),(M /. 1)))) & (M /. 1) in ( L~ M) by A31, JORDAN3: 1, SPPOL_2: 20;

        hence contradiction by A65, A55, A64, A62, A57, Th29, ZFMISC_1: 125;

      end;

    end;

    theorem :: SPRECT_2:72

    

     Th72: (z /. 1) = ( N-min ( L~ z)) & ( E-min ( L~ z)) <> ( S-max ( L~ z)) implies (( E-min ( L~ z)) .. z) < (( S-max ( L~ z)) .. z)

    proof

      set i1 = (( E-min ( L~ z)) .. z), i2 = (( S-max ( L~ z)) .. z);

      assume that

       A1: (z /. 1) = ( N-min ( L~ z)) and

       A2: ( E-min ( L~ z)) <> ( S-max ( L~ z)) & i1 >= i2;

      

       A3: ( S-bound ( L~ z)) < ( N-bound ( L~ z)) by TOPREAL5: 16;

      (z /. 2) in ( N-most ( L~ z)) by A1, Th30;

      

      then

       A4: ((z /. 2) `2 ) = (( N-min ( L~ z)) `2 ) by PSCOMP_1: 39

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

      

       A5: ( S-max ( L~ z)) in ( rng z) by Th42;

      then

       A6: i2 in ( dom z) by FINSEQ_4: 20;

      then

       A7: i2 <= ( len z) by FINSEQ_3: 25;

      

       A8: (z /. i2) = (z . i2) by A6, PARTFUN1:def 6

      .= ( S-max ( L~ z)) by A5, FINSEQ_4: 19;

      then

       A9: ((z /. i2) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      

       A10: 1 <= i2 by A6, FINSEQ_3: 25;

      

       A11: i2 <> 0 by A6, FINSEQ_3: 25;

      ((z /. 1) `2 ) = ( N-bound ( L~ z)) by A1, EUCLID: 52;

      then i2 <> 0 & ... & i2 <> 2 by A4, A11, A9, A3;

      then

       A12: i2 > 2;

      then

      reconsider h = ( mid (z,i2,2)) as S-Sequence_in_R2 by A7, Th37;

      

       A13: 2 <= ( len z) by NAT_D: 60;

      then

       A14: 2 in ( dom z) by FINSEQ_3: 25;

      then (h /. 1) = ( S-max ( L~ z)) by A6, A8, Th8;

      then

       A15: ((h /. 1) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      h is_in_the_area_of z & (h /. ( len h)) = (z /. 2) by A6, A14, Th9, Th21, Th22;

      then

       A16: ( len h) >= 2 & h is_a_v.c._for z by A4, A15, TOPREAL1:def 8;

      ( N-max ( L~ z)) in ( L~ z) by SPRECT_1: 11;

      then (( N-max ( L~ z)) `1 ) <= ( E-bound ( L~ z)) by PSCOMP_1: 24;

      then (( N-min ( L~ z)) `1 ) < ( E-bound ( L~ z)) by Th51, XXREAL_0: 2;

      then

       A17: (( N-min ( L~ z)) `1 ) < (( E-min ( L~ z)) `1 ) by EUCLID: 52;

      

       A18: ( E-min ( L~ z)) in ( rng z) by Th45;

      then

       A19: i1 in ( dom z) by FINSEQ_4: 20;

      

      then

       A20: (z /. i1) = (z . i1) by PARTFUN1:def 6

      .= ( E-min ( L~ z)) by A18, FINSEQ_4: 19;

      

       A21: i1 <= ( len z) by A19, FINSEQ_3: 25;

      (z /. ( len z)) = ( N-min ( L~ z)) by A1, FINSEQ_6:def 1;

      then

       A22: i1 < ( len z) by A21, A20, A17, XXREAL_0: 1;

      then (i1 + 1) <= ( len z) by NAT_1: 13;

      then (( len z) - i1) >= 1 by XREAL_1: 19;

      then (( len z) -' i1) >= 1 by NAT_D: 39;

      then

       A23: ((( len z) -' i1) + 1) >= (1 + 1) by XREAL_1: 6;

      

       A24: i1 > i2 by A2, A8, A20, XXREAL_0: 1;

      then i1 > 1 by A10, XXREAL_0: 2;

      then

      reconsider M = ( mid (z,( len z),i1)) as S-Sequence_in_R2 by A22, Th37;

      

       A25: ( len z) in ( dom z) by FINSEQ_5: 6;

      

      then

       A26: (M /. ( len M)) = (z /. i1) by A19, Th9

      .= ( E-min ( L~ z)) by A18, FINSEQ_5: 38;

      1 <= i1 by A19, FINSEQ_3: 25;

      then

       A27: ( len M) = ((( len z) -' i1) + 1) by A21, JORDAN4: 9;

      

       A28: ( L~ M) misses ( L~ h) by A21, A24, A12, Th49;

      

       A29: (z /. 1) = (z /. ( len z)) by FINSEQ_6:def 1;

      then

       A30: (M /. 1) = (z /. 1) by A19, A25, Th8;

      per cases ;

        suppose that

         A31: ( NW-corner ( L~ z)) = ( N-min ( L~ z));

        (M /. 1) = (z /. ( len z)) by A19, A25, Th8;

        then

         A32: ((M /. 1) `1 ) = ( W-bound ( L~ z)) by A1, A29, A31, EUCLID: 52;

        M is_in_the_area_of z & ((M /. ( len M)) `1 ) = ( E-bound ( L~ z)) by A19, A25, A26, Th21, Th22, EUCLID: 52;

        then M is_a_h.c._for z by A32;

        hence contradiction by A16, A28, A27, A23, Th29;

      end;

        suppose ( NW-corner ( L~ z)) <> ( N-min ( L~ z));

        then

        reconsider g = ( <*( NW-corner ( L~ z))*> ^ M) as S-Sequence_in_R2 by A1, A19, A25, A29, Th66;

        

         A33: ( len g) >= 2 & ( L~ g) = (( L~ M) \/ ( LSeg (( NW-corner ( L~ z)),(M /. 1)))) by SPPOL_2: 20, TOPREAL1:def 8;

        (g /. 1) = ( NW-corner ( L~ z)) by FINSEQ_5: 15;

        then

         A34: ((g /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

        (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ z)) by A10, A7, A13, JORDAN4: 35, XBOOLE_1: 26;

        then

         A35: (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. 1)} by A1, A30, PSCOMP_1: 43;

        ( len M) in ( dom M) & ( len g) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22, FINSEQ_5: 6;

        

        then (g /. ( len g)) = (M /. ( len M)) by FINSEQ_4: 69

        .= (z /. i1) by A19, A25, Th9

        .= ( E-min ( L~ z)) by A18, FINSEQ_5: 38;

        then

         A36: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

        

         A37: (M /. 1) in ( L~ M) by A27, A23, JORDAN3: 1;

        M is_in_the_area_of z & <*( NW-corner ( L~ z))*> is_in_the_area_of z by A19, A25, Th21, Th22, Th26;

        then g is_in_the_area_of z by Th24;

        then g is_a_h.c._for z by A34, A36;

        hence contradiction by A16, A28, A33, A35, A37, Th29, ZFMISC_1: 125;

      end;

    end;

    theorem :: SPRECT_2:73

    

     Th73: (z /. 1) = ( N-min ( L~ z)) implies (( S-max ( L~ z)) .. z) < (( S-min ( L~ z)) .. z)

    proof

      set i1 = (( S-max ( L~ z)) .. z), i2 = (( S-min ( L~ z)) .. z), j = (( N-max ( L~ z)) .. z);

      assume that

       A1: (z /. 1) = ( N-min ( L~ z)) and

       A2: i1 >= i2;

      

       A3: (z /. 1) = (z /. ( len z)) by FINSEQ_6:def 1;

      

       A4: ( S-min ( L~ z)) in ( rng z) by Th41;

      then

       A5: i2 in ( dom z) by FINSEQ_4: 20;

      then

       A6: i2 <= ( len z) by FINSEQ_3: 25;

      

       A7: 1 <= i2 by A5, FINSEQ_3: 25;

      

       A8: ( S-max ( L~ z)) in ( rng z) by Th42;

      then

       A9: i1 in ( dom z) by FINSEQ_4: 20;

      

      then

       A10: (z /. i1) = (z . i1) by PARTFUN1:def 6

      .= ( S-max ( L~ z)) by A8, FINSEQ_4: 19;

      

       A11: i1 <= ( len z) by A9, FINSEQ_3: 25;

      (( N-min ( L~ z)) `2 ) = ( N-bound ( L~ z)) & (( S-max ( L~ z)) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      then ( N-min ( L~ z)) <> ( S-max ( L~ z)) by TOPREAL5: 16;

      then

       A12: i1 < ( len z) by A1, A11, A10, A3, XXREAL_0: 1;

      then (i1 + 1) <= ( len z) by NAT_1: 13;

      then (( len z) - i1) >= 1 by XREAL_1: 19;

      then (( len z) -' i1) >= 1 by NAT_D: 39;

      then

       A13: ((( len z) -' i1) + 1) >= (1 + 1) by XREAL_1: 6;

      

       A14: ( N-max ( L~ z)) in ( rng z) by Th40;

      then

       A15: j in ( dom z) by FINSEQ_4: 20;

      then

       A16: 1 <= j by FINSEQ_3: 25;

      then i1 > 1 by A1, Lm5, XXREAL_0: 2;

      then

      reconsider M = ( mid (z,( len z),i1)) as S-Sequence_in_R2 by A12, Th37;

      

       A17: (z /. j) = (z . j) by A15, PARTFUN1:def 6

      .= ( N-max ( L~ z)) by A14, FINSEQ_4: 19;

      then

       A18: ((z /. j) `2 ) = ( N-bound ( L~ z)) by EUCLID: 52;

      ( N-min ( L~ z)) <> ( N-max ( L~ z)) by Th52;

      then

       A19: 1 < j by A1, A16, A17, XXREAL_0: 1;

      

       A20: ( len z) in ( dom z) by FINSEQ_5: 6;

      then

       A21: (M /. 1) = (z /. ( len z)) by A9, Th8;

      1 <= i1 by A9, FINSEQ_3: 25;

      then

       A22: ( len M) = ((( len z) -' i1) + 1) by A11, JORDAN4: 9;

      then

       A23: (M /. ( len M)) in ( L~ M) by A13, JORDAN3: 1;

      

       A24: 1 in ( dom M) by FINSEQ_5: 6;

      

       A25: j <= ( len z) by A15, FINSEQ_3: 25;

      

       A26: i2 > j by A1, Lm6;

      then

      reconsider h = ( mid (z,i2,j)) as S-Sequence_in_R2 by A6, A19, Th37;

      

       A27: (z /. i2) = (z . i2) by A5, PARTFUN1:def 6

      .= ( S-min ( L~ z)) by A4, FINSEQ_4: 19;

      then (h /. 1) = ( S-min ( L~ z)) by A5, A15, Th8;

      then

       A28: ((h /. 1) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      h is_in_the_area_of z & (h /. ( len h)) = (z /. j) by A5, A15, Th9, Th21, Th22;

      then

       A29: ( len h) >= 2 & h is_a_v.c._for z by A18, A28, TOPREAL1:def 8;

      ( S-min ( L~ z)) <> ( S-max ( L~ z)) by Th56;

      then i1 > i2 by A2, A27, A10, XXREAL_0: 1;

      then

       A30: ( L~ h) misses ( L~ M) by A11, A26, A19, Th49;

      

       A31: (M /. ( len M)) = ( S-max ( L~ z)) by A9, A10, A20, Th9;

      per cases ;

        suppose that

         A32: ( NW-corner ( L~ z)) = ( N-min ( L~ z)) & ( SE-corner ( L~ z)) = ( S-max ( L~ z));

        

         A33: M is_in_the_area_of z by A9, A20, Th21, Th22;

        ((M /. 1) `1 ) = ( W-bound ( L~ z)) & ((M /. ( len M)) `1 ) = ( E-bound ( L~ z)) by A1, A3, A31, A21, A32, EUCLID: 52;

        then M is_a_h.c._for z by A33;

        hence contradiction by A29, A30, A22, A13, Th29;

      end;

        suppose that

         A34: ( NW-corner ( L~ z)) = ( N-min ( L~ z)) and

         A35: ( SE-corner ( L~ z)) <> ( S-max ( L~ z));

        reconsider g = (M ^ <*( SE-corner ( L~ z))*>) as S-Sequence_in_R2 by A9, A10, A20, A35, Th64;

        

         A36: ( len g) >= 2 & ( L~ g) = (( L~ M) \/ ( LSeg ((M /. ( len M)),( SE-corner ( L~ z))))) by SPPOL_2: 19, TOPREAL1:def 8;

        ( len g) = (( len M) + ( len <*( SE-corner ( L~ z))*>)) by FINSEQ_1: 22

        .= (( len M) + 1) by FINSEQ_1: 39;

        then (g /. ( len g)) = ( SE-corner ( L~ z)) by FINSEQ_4: 67;

        then

         A37: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

        M is_in_the_area_of z & <*( SE-corner ( L~ z))*> is_in_the_area_of z by A9, A20, Th21, Th22, Th27;

        then

         A38: g is_in_the_area_of z by Th24;

        (( LSeg ((M /. ( len M)),( SE-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. ( len M)),( SE-corner ( L~ z)))) /\ ( L~ z)) by A7, A6, A16, A25, JORDAN4: 35, XBOOLE_1: 26;

        then

         A39: (( LSeg ((M /. ( len M)),( SE-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. ( len M))} by A31, PSCOMP_1: 59;

        (g /. 1) = (M /. 1) by A24, FINSEQ_4: 68

        .= (z /. 1) by A9, A3, A20, Th8;

        then ((g /. 1) `1 ) = ( W-bound ( L~ z)) by A1, A34, EUCLID: 52;

        then g is_a_h.c._for z by A38, A37;

        hence contradiction by A29, A30, A23, A36, A39, Th29, ZFMISC_1: 125;

      end;

        suppose that

         A40: ( NW-corner ( L~ z)) <> ( N-min ( L~ z)) and

         A41: ( SE-corner ( L~ z)) = ( S-max ( L~ z));

        reconsider g = ( <*( NW-corner ( L~ z))*> ^ M) as S-Sequence_in_R2 by A1, A9, A3, A20, A40, Th66;

        ( len M) in ( dom M) & ( len g) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22, FINSEQ_5: 6;

        

        then (g /. ( len g)) = (M /. ( len M)) by FINSEQ_4: 69

        .= ( S-max ( L~ z)) by A9, A10, A20, Th9;

        then

         A42: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by A41, EUCLID: 52;

        

         A43: ( len g) >= 2 & ( L~ g) = (( L~ M) \/ ( LSeg (( NW-corner ( L~ z)),(M /. 1)))) by SPPOL_2: 20, TOPREAL1:def 8;

        (g /. 1) = ( NW-corner ( L~ z)) by FINSEQ_5: 15;

        then

         A44: ((g /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

        (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ z)) by A7, A6, A16, A25, JORDAN4: 35, XBOOLE_1: 26;

        then

         A45: (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. 1)} by A1, A3, A21, PSCOMP_1: 43;

        

         A46: (M /. 1) in ( L~ M) by A22, A13, JORDAN3: 1;

        M is_in_the_area_of z & <*( NW-corner ( L~ z))*> is_in_the_area_of z by A9, A20, Th21, Th22, Th26;

        then g is_in_the_area_of z by Th24;

        then g is_a_h.c._for z by A44, A42;

        hence contradiction by A29, A30, A43, A45, A46, Th29, ZFMISC_1: 125;

      end;

        suppose that

         A47: ( NW-corner ( L~ z)) <> ( N-min ( L~ z)) & ( SE-corner ( L~ z)) <> ( S-max ( L~ z));

        set K = ( <*( NW-corner ( L~ z))*> ^ M);

        reconsider g = (K ^ <*( SE-corner ( L~ z))*>) as S-Sequence_in_R2 by A1, A9, A10, A3, A20, A47, Lm3;

        1 in ( dom ( <*( NW-corner ( L~ z))*> ^ M)) by FINSEQ_5: 6;

        

        then (g /. 1) = (( <*( NW-corner ( L~ z))*> ^ M) /. 1) by FINSEQ_4: 68

        .= ( NW-corner ( L~ z)) by FINSEQ_5: 15;

        then

         A48: ((g /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

        ( len g) = (( len ( <*( NW-corner ( L~ z))*> ^ M)) + ( len <*( SE-corner ( L~ z))*>)) by FINSEQ_1: 22

        .= (( len ( <*( NW-corner ( L~ z))*> ^ M)) + 1) by FINSEQ_1: 39;

        then (g /. ( len g)) = ( SE-corner ( L~ z)) by FINSEQ_4: 67;

        then

         A49: ((g /. ( len g)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

        M is_in_the_area_of z & <*( NW-corner ( L~ z))*> is_in_the_area_of z by A9, A20, Th21, Th22, Th26;

        then

         A50: ( <*( NW-corner ( L~ z))*> ^ M) is_in_the_area_of z by Th24;

         <*( SE-corner ( L~ z))*> is_in_the_area_of z by Th27;

        then g is_in_the_area_of z by A50, Th24;

        then

         A51: g is_a_h.c._for z by A48, A49;

        ( len K) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22;

        then ( len K) >= ( len M) by NAT_1: 11;

        then ( len K) >= 2 by A22, A13, XXREAL_0: 2;

        then

         A52: (K /. ( len K)) in ( L~ K) by JORDAN3: 1;

        (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ z)) by A7, A6, A16, A25, JORDAN4: 35, XBOOLE_1: 26;

        then

         A53: (( LSeg ((M /. 1),( NW-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. 1)} by A1, A3, A21, PSCOMP_1: 43;

        ( L~ K) = (( L~ M) \/ ( LSeg (( NW-corner ( L~ z)),(M /. 1)))) & (M /. 1) in ( L~ M) by A22, A13, JORDAN3: 1, SPPOL_2: 20;

        then

         A54: ( L~ K) misses ( L~ h) by A30, A53, ZFMISC_1: 125;

        ( len M) in ( dom M) & ( len K) = (( len M) + ( len <*( NW-corner ( L~ z))*>)) by FINSEQ_1: 22, FINSEQ_5: 6;

        

        then

         A55: (K /. ( len K)) = (M /. ( len M)) by FINSEQ_4: 69

        .= (z /. i1) by A9, A20, Th9

        .= ( S-max ( L~ z)) by A8, FINSEQ_5: 38;

        (( LSeg ((K /. ( len K)),( SE-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((K /. ( len K)),( SE-corner ( L~ z)))) /\ ( L~ z)) by A7, A6, A16, A25, JORDAN4: 35, XBOOLE_1: 26;

        then

         A56: (( LSeg ((K /. ( len K)),( SE-corner ( L~ z)))) /\ ( L~ h)) c= {(K /. ( len K))} by A55, PSCOMP_1: 59;

        ( len g) >= 2 & ( L~ g) = (( L~ K) \/ ( LSeg ((K /. ( len K)),( SE-corner ( L~ z))))) by SPPOL_2: 19, TOPREAL1:def 8;

        hence contradiction by A29, A51, A54, A52, A56, Th29, ZFMISC_1: 125;

      end;

    end;

    

     Lm9: (z /. 1) = ( N-min ( L~ z)) implies (( E-min ( L~ z)) .. z) < (( S-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( N-min ( L~ z));

      then (( E-min ( L~ z)) .. z) <= (( S-max ( L~ z)) .. z) by Th72;

      hence thesis by A1, Th73, XXREAL_0: 2;

    end;

    

     Lm10: (z /. 1) = ( N-min ( L~ z)) & ( N-min ( L~ z)) <> ( W-max ( L~ z)) implies (( E-min ( L~ z)) .. z) < (( W-max ( L~ z)) .. z)

    proof

      set i1 = (( E-min ( L~ z)) .. z), i2 = (( W-max ( L~ z)) .. z), j = (( S-min ( L~ z)) .. z);

      assume that

       A1: (z /. 1) = ( N-min ( L~ z)) and

       A2: ( N-min ( L~ z)) <> ( W-max ( L~ z)) and

       A3: i1 >= i2;

      

       A4: (z /. ( len z)) = ( N-min ( L~ z)) by A1, FINSEQ_6:def 1;

      ( N-max ( L~ z)) in ( L~ z) by SPRECT_1: 11;

      then (( N-max ( L~ z)) `1 ) <= ( E-bound ( L~ z)) by PSCOMP_1: 24;

      then (( N-min ( L~ z)) `1 ) < ( E-bound ( L~ z)) by Th51, XXREAL_0: 2;

      then

       A5: (( N-min ( L~ z)) `1 ) < (( E-min ( L~ z)) `1 ) by EUCLID: 52;

      (( N-min ( L~ z)) `2 ) = ( N-bound ( L~ z)) & (( S-min ( L~ z)) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      then

       A6: ( N-min ( L~ z)) <> ( S-min ( L~ z)) by TOPREAL5: 16;

      

       A7: ( S-min ( L~ z)) in ( rng z) by Th41;

      then

       A8: j in ( dom z) by FINSEQ_4: 20;

      then

       A9: j <= ( len z) by FINSEQ_3: 25;

      

       A10: ( E-min ( L~ z)) in ( rng z) by Th45;

      then

       A11: i1 in ( dom z) by FINSEQ_4: 20;

      

      then

       A12: (z /. i1) = (z . i1) by PARTFUN1:def 6

      .= ( E-min ( L~ z)) by A10, FINSEQ_4: 19;

      

       A13: ( W-max ( L~ z)) in ( rng z) by Th44;

      then

       A14: i2 in ( dom z) by FINSEQ_4: 20;

      

      then

       A15: (z /. i2) = (z . i2) by PARTFUN1:def 6

      .= ( W-max ( L~ z)) by A13, FINSEQ_4: 19;

      

       A16: 1 <= i2 by A14, FINSEQ_3: 25;

      (( W-max ( L~ z)) `1 ) = ( W-bound ( L~ z)) & (( E-min ( L~ z)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

      then (( W-max ( L~ z)) `1 ) < (( E-min ( L~ z)) `1 ) by TOPREAL5: 17;

      then

       A17: i1 > i2 by A3, A15, A12, XXREAL_0: 1;

      then i1 > 1 by A16, XXREAL_0: 2;

      then

       A18: j > 1 by A1, Lm9, XXREAL_0: 2;

      (z /. j) = (z . j) by A8, PARTFUN1:def 6

      .= ( S-min ( L~ z)) by A7, FINSEQ_4: 19;

      then j < ( len z) by A4, A9, A6, XXREAL_0: 1;

      then

      reconsider h = ( mid (z,j,( len z))) as S-Sequence_in_R2 by A18, Th38;

      

       A19: i1 < j by A1, Lm9;

      

       A20: ( len z) in ( dom z) by FINSEQ_5: 6;

      then (h /. ( len h)) = (z /. ( len z)) by A8, Th9;

      then

       A21: ((h /. ( len h)) `2 ) = ( N-bound ( L~ z)) by A4, EUCLID: 52;

      i1 <= ( len z) by A11, FINSEQ_3: 25;

      then i1 < ( len z) by A4, A12, A5, XXREAL_0: 1;

      then

      reconsider M = ( mid (z,i2,i1)) as S-Sequence_in_R2 by A16, A17, Th38;

      (M /. ( len M)) = (z /. i1) by A11, A14, Th9

      .= ( E-min ( L~ z)) by A10, FINSEQ_5: 38;

      then

       A22: ((M /. ( len M)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

      (M /. 1) = ( W-max ( L~ z)) by A11, A14, A15, Th8;

      then

       A23: ((M /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

      M is_in_the_area_of z by A11, A14, Th21, Th22;

      then

       A24: M is_a_h.c._for z by A23, A22;

      (z /. j) = (z . j) by A8, PARTFUN1:def 6

      .= ( S-min ( L~ z)) by A7, FINSEQ_4: 19;

      then (h /. 1) = ( S-min ( L~ z)) by A20, A8, Th8;

      then

       A25: ((h /. 1) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      h is_in_the_area_of z by A20, A8, Th21, Th22;

      then

       A26: h is_a_v.c._for z by A25, A21;

      i2 > 1 by A1, A2, A16, A15, XXREAL_0: 1;

      then

       A27: ( L~ M) misses ( L~ h) by A3, A9, A19, Th47;

      ( len h) >= 2 & ( len M) >= 2 by TOPREAL1:def 8;

      hence contradiction by A26, A24, A27, Th29;

    end;

    

     Lm11: (z /. 1) = ( N-min ( L~ z)) implies (( E-min ( L~ z)) .. z) < (( W-min ( L~ z)) .. z)

    proof

      set i1 = (( E-min ( L~ z)) .. z), i2 = (( W-min ( L~ z)) .. z), j = (( S-min ( L~ z)) .. z);

      assume that

       A1: (z /. 1) = ( N-min ( L~ z)) and

       A2: i1 >= i2;

      

       A3: (z /. ( len z)) = ( N-min ( L~ z)) by A1, FINSEQ_6:def 1;

      ( N-max ( L~ z)) in ( L~ z) by SPRECT_1: 11;

      then (( N-max ( L~ z)) `1 ) <= ( E-bound ( L~ z)) by PSCOMP_1: 24;

      then (( N-min ( L~ z)) `1 ) < ( E-bound ( L~ z)) by Th51, XXREAL_0: 2;

      then

       A4: (( N-min ( L~ z)) `1 ) < (( E-min ( L~ z)) `1 ) by EUCLID: 52;

      (( N-min ( L~ z)) `2 ) = ( N-bound ( L~ z)) & (( S-min ( L~ z)) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      then

       A5: ( N-min ( L~ z)) <> ( S-min ( L~ z)) by TOPREAL5: 16;

      

       A6: ( S-min ( L~ z)) in ( rng z) by Th41;

      then

       A7: j in ( dom z) by FINSEQ_4: 20;

      then

       A8: j <= ( len z) by FINSEQ_3: 25;

      

       A9: ( E-min ( L~ z)) in ( rng z) by Th45;

      then

       A10: i1 in ( dom z) by FINSEQ_4: 20;

      

      then

       A11: (z /. i1) = (z . i1) by PARTFUN1:def 6

      .= ( E-min ( L~ z)) by A9, FINSEQ_4: 19;

      

       A12: ( W-min ( L~ z)) in ( rng z) by Th43;

      then

       A13: i2 in ( dom z) by FINSEQ_4: 20;

      

      then

       A14: (z /. i2) = (z . i2) by PARTFUN1:def 6

      .= ( W-min ( L~ z)) by A12, FINSEQ_4: 19;

      

       A15: 1 <= i2 by A13, FINSEQ_3: 25;

      (( W-min ( L~ z)) `1 ) = ( W-bound ( L~ z)) & (( E-min ( L~ z)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

      then (z /. i1) <> (z /. i2) by A14, A11, TOPREAL5: 17;

      then

       A16: i1 > i2 by A2, XXREAL_0: 1;

      then i1 > 1 by A15, XXREAL_0: 2;

      then

       A17: j > 1 by A1, Lm9, XXREAL_0: 2;

      (z /. j) = (z . j) by A7, PARTFUN1:def 6

      .= ( S-min ( L~ z)) by A6, FINSEQ_4: 19;

      then j < ( len z) by A3, A8, A5, XXREAL_0: 1;

      then

      reconsider h = ( mid (z,j,( len z))) as S-Sequence_in_R2 by A17, Th38;

      

       A18: i1 < j by A1, Lm9;

      

       A19: ( len z) in ( dom z) by FINSEQ_5: 6;

      then (h /. ( len h)) = (z /. ( len z)) by A7, Th9;

      then

       A20: ((h /. ( len h)) `2 ) = ( N-bound ( L~ z)) by A3, EUCLID: 52;

      i1 <= ( len z) by A10, FINSEQ_3: 25;

      then i1 < ( len z) by A3, A11, A4, XXREAL_0: 1;

      then

      reconsider M = ( mid (z,i2,i1)) as S-Sequence_in_R2 by A15, A16, Th38;

      (M /. ( len M)) = (z /. i1) by A10, A13, Th9

      .= ( E-min ( L~ z)) by A9, FINSEQ_5: 38;

      then

       A21: ((M /. ( len M)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

      (z /. j) = (z . j) by A7, PARTFUN1:def 6

      .= ( S-min ( L~ z)) by A6, FINSEQ_4: 19;

      then (h /. 1) = ( S-min ( L~ z)) by A19, A7, Th8;

      then

       A22: ((h /. 1) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      h is_in_the_area_of z by A19, A7, Th21, Th22;

      then

       A23: h is_a_v.c._for z by A22, A20;

      ( W-max ( L~ z)) in ( L~ z) & (( N-min ( L~ z)) `2 ) = ( N-bound ( L~ z)) by EUCLID: 52, SPRECT_1: 13;

      then (( W-max ( L~ z)) `2 ) <= (( N-min ( L~ z)) `2 ) by PSCOMP_1: 24;

      then ( N-min ( L~ z)) <> ( W-min ( L~ z)) by Th57;

      then i2 > 1 by A1, A15, A14, XXREAL_0: 1;

      then

       A24: ( L~ M) misses ( L~ h) by A2, A8, A18, Th47;

      (M /. 1) = ( W-min ( L~ z)) by A10, A13, A14, Th8;

      then

       A25: ((M /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

      M is_in_the_area_of z by A10, A13, Th21, Th22;

      then

       A26: M is_a_h.c._for z by A25, A21;

      ( len h) >= 2 & ( len M) >= 2 by TOPREAL1:def 8;

      hence contradiction by A23, A26, A24, Th29;

    end;

    theorem :: SPRECT_2:74

    (z /. 1) = ( N-min ( L~ z)) & ( S-min ( L~ z)) <> ( W-min ( L~ z)) implies (( S-min ( L~ z)) .. z) < (( W-min ( L~ z)) .. z)

    proof

      set i1 = (( E-min ( L~ z)) .. z), i2 = (( W-min ( L~ z)) .. z), j = (( S-min ( L~ z)) .. z);

      assume that

       A1: (z /. 1) = ( N-min ( L~ z)) and

       A2: ( S-min ( L~ z)) <> ( W-min ( L~ z)) & j >= i2;

      

       A3: (z /. ( len z)) = ( N-min ( L~ z)) by A1, FINSEQ_6:def 1;

      ( N-max ( L~ z)) in ( L~ z) by SPRECT_1: 11;

      then (( N-max ( L~ z)) `1 ) <= ( E-bound ( L~ z)) by PSCOMP_1: 24;

      then (( N-min ( L~ z)) `1 ) < ( E-bound ( L~ z)) by Th51, XXREAL_0: 2;

      then

       A4: (( N-min ( L~ z)) `1 ) < (( E-min ( L~ z)) `1 ) by EUCLID: 52;

      

       A5: ( E-min ( L~ z)) in ( rng z) by Th45;

      then

       A6: i1 in ( dom z) by FINSEQ_4: 20;

      then

       A7: 1 <= i1 by FINSEQ_3: 25;

      then

       A8: j > 1 by A1, Lm9, XXREAL_0: 2;

      (z /. i1) = (z . i1) by A6, PARTFUN1:def 6

      .= ( E-min ( L~ z)) by A5, FINSEQ_4: 19;

      then

       A9: i1 > 1 by A1, A7, A4, XXREAL_0: 1;

      (( N-min ( L~ z)) `2 ) = ( N-bound ( L~ z)) & (( S-min ( L~ z)) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      then

       A10: ( N-min ( L~ z)) <> ( S-min ( L~ z)) by TOPREAL5: 16;

      

       A11: ( S-min ( L~ z)) in ( rng z) by Th41;

      then

       A12: j in ( dom z) by FINSEQ_4: 20;

      then

       A13: j <= ( len z) by FINSEQ_3: 25;

      (z /. j) = (z . j) by A12, PARTFUN1:def 6

      .= ( S-min ( L~ z)) by A11, FINSEQ_4: 19;

      then j < ( len z) by A3, A13, A10, XXREAL_0: 1;

      then

      reconsider h = ( mid (z,j,( len z))) as S-Sequence_in_R2 by A8, Th38;

      

       A14: ( len z) in ( dom z) by FINSEQ_5: 6;

      then (h /. ( len h)) = (z /. ( len z)) by A12, Th9;

      then

       A15: ((h /. ( len h)) `2 ) = ( N-bound ( L~ z)) by A3, EUCLID: 52;

      

       A16: (z /. j) = (z . j) by A12, PARTFUN1:def 6

      .= ( S-min ( L~ z)) by A11, FINSEQ_4: 19;

      then (h /. 1) = ( S-min ( L~ z)) by A12, A14, Th8;

      then

       A17: ((h /. 1) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

      h is_in_the_area_of z by A12, A14, Th21, Th22;

      then

       A18: h is_a_v.c._for z by A17, A15;

      

       A19: i1 < i2 by A1, Lm11;

      

       A20: ( W-min ( L~ z)) in ( rng z) by Th43;

      then

       A21: i2 in ( dom z) by FINSEQ_4: 20;

      then i2 <= ( len z) by FINSEQ_3: 25;

      then

      reconsider M = ( mid (z,i2,i1)) as S-Sequence_in_R2 by A19, A9, Th37;

      (M /. ( len M)) = (z /. i1) by A6, A21, Th9

      .= ( E-min ( L~ z)) by A5, FINSEQ_5: 38;

      then

       A22: ((M /. ( len M)) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

      

       A23: (z /. i2) = (z . i2) by A21, PARTFUN1:def 6

      .= ( W-min ( L~ z)) by A20, FINSEQ_4: 19;

      then (M /. 1) = ( W-min ( L~ z)) by A6, A21, Th8;

      then

       A24: ((M /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

      M is_in_the_area_of z by A6, A21, Th21, Th22;

      then

       A25: M is_a_h.c._for z by A24, A22;

      

       A26: ( len h) >= 2 & ( len M) >= 2 by TOPREAL1:def 8;

      j > i2 by A2, A23, A16, XXREAL_0: 1;

      then ( L~ M) misses ( L~ h) by A19, A9, A13, Th50;

      hence contradiction by A18, A26, A25, Th29;

    end;

    theorem :: SPRECT_2:75

    

     Th75: (z /. 1) = ( N-min ( L~ z)) & ( N-min ( L~ z)) <> ( W-max ( L~ z)) implies (( W-min ( L~ z)) .. z) < (( W-max ( L~ z)) .. z)

    proof

      set i1 = (( W-min ( L~ z)) .. z), i2 = (( W-max ( L~ z)) .. z), j = (( E-min ( L~ z)) .. z);

      assume that

       A1: (z /. 1) = ( N-min ( L~ z)) and

       A2: ( N-min ( L~ z)) <> ( W-max ( L~ z)) and

       A3: i1 >= i2;

      

       A4: i2 > j by A1, A2, Lm10;

      

       A5: ( E-min ( L~ z)) in ( rng z) by Th45;

      then

       A6: j in ( dom z) by FINSEQ_4: 20;

      

      then

       A7: (z /. j) = (z . j) by PARTFUN1:def 6

      .= ( E-min ( L~ z)) by A5, FINSEQ_4: 19;

      then

       A8: ((z /. j) `1 ) = ( E-bound ( L~ z)) by EUCLID: 52;

      

       A9: j <= ( len z) by A6, FINSEQ_3: 25;

      

       A10: (z /. ( len z)) = ( N-min ( L~ z)) by A1, FINSEQ_6:def 1;

      

       A11: ( W-max ( L~ z)) in ( rng z) by Th44;

      then

       A12: i2 in ( dom z) by FINSEQ_4: 20;

      then

       A13: 1 <= i2 by FINSEQ_3: 25;

      

       A14: ( W-min ( L~ z)) in ( rng z) by Th43;

      then

       A15: i1 in ( dom z) by FINSEQ_4: 20;

      

      then

       A16: (z /. i1) = (z . i1) by PARTFUN1:def 6

      .= ( W-min ( L~ z)) by A14, FINSEQ_4: 19;

      

       A17: i1 <= ( len z) by A15, FINSEQ_3: 25;

      ( W-max ( L~ z)) in ( L~ z) & (( N-min ( L~ z)) `2 ) = ( N-bound ( L~ z)) by EUCLID: 52, SPRECT_1: 13;

      then (( W-max ( L~ z)) `2 ) <= (( N-min ( L~ z)) `2 ) by PSCOMP_1: 24;

      then (z /. 1) = (z /. ( len z)) & ( N-min ( L~ z)) <> ( W-min ( L~ z)) by Th57, FINSEQ_6:def 1;

      then

       A18: i1 < ( len z) by A1, A17, A16, XXREAL_0: 1;

      then (i1 + 1) <= ( len z) by NAT_1: 13;

      then (( len z) - i1) >= 1 by XREAL_1: 19;

      then (( len z) -' i1) >= 1 by NAT_D: 39;

      then

       A19: ((( len z) -' i1) + 1) >= (1 + 1) by XREAL_1: 6;

      

       A20: 1 <= j by A6, FINSEQ_3: 25;

      then i1 > 1 by A1, Lm11, XXREAL_0: 2;

      then

      reconsider M = ( mid (z,i1,( len z))) as S-Sequence_in_R2 by A18, Th38;

      

       A21: ( len z) in ( dom z) by FINSEQ_5: 6;

      then

       A22: (M /. 1) = (z /. i1) by A15, Th8;

      1 <= i1 by A15, FINSEQ_3: 25;

      then

       A23: ( len M) = ((( len z) -' i1) + 1) by A17, JORDAN4: 8;

      

       A24: M is_in_the_area_of z by A15, A21, Th21, Th22;

      

       A25: (M /. ( len M)) = (z /. ( len z)) by A15, A21, Th9;

      ( N-max ( L~ z)) in ( L~ z) by SPRECT_1: 11;

      then (( N-max ( L~ z)) `1 ) <= ( E-bound ( L~ z)) by PSCOMP_1: 24;

      then (( N-min ( L~ z)) `1 ) < ( E-bound ( L~ z)) by Th51, XXREAL_0: 2;

      then (( N-min ( L~ z)) `1 ) < (( E-min ( L~ z)) `1 ) by EUCLID: 52;

      then

       A26: 1 < j by A1, A20, A7, XXREAL_0: 1;

      

       A27: i2 <= ( len z) by A12, FINSEQ_3: 25;

      then

      reconsider h = ( mid (z,i2,j)) as S-Sequence_in_R2 by A4, A26, Th37;

      

       A28: (z /. i2) = (z . i2) by A12, PARTFUN1:def 6

      .= ( W-max ( L~ z)) by A11, FINSEQ_4: 19;

      then (h /. 1) = ( W-max ( L~ z)) by A12, A6, Th8;

      then

       A29: ((h /. 1) `1 ) = ( W-bound ( L~ z)) by EUCLID: 52;

      h is_in_the_area_of z & (h /. ( len h)) = (z /. j) by A12, A6, Th9, Th21, Th22;

      then

       A30: ( len h) >= 2 & h is_a_h.c._for z by A8, A29, TOPREAL1:def 8;

      ( W-max ( L~ z)) <> ( W-min ( L~ z)) by Th58;

      then i1 > i2 by A3, A28, A16, XXREAL_0: 1;

      then

       A31: ( L~ M) misses ( L~ h) by A17, A4, A26, Th50;

      per cases ;

        suppose

         A32: ( SW-corner ( L~ z)) = ( W-min ( L~ z));

        

         A33: ((M /. ( len M)) `2 ) = ( N-bound ( L~ z)) by A10, A25, EUCLID: 52;

        ((M /. 1) `2 ) = ( S-bound ( L~ z)) by A16, A22, A32, EUCLID: 52;

        then M is_a_v.c._for z by A24, A33;

        hence contradiction by A30, A31, A23, A19, Th29;

      end;

        suppose ( SW-corner ( L~ z)) <> ( W-min ( L~ z));

        then

        reconsider g = ( <*( SW-corner ( L~ z))*> ^ M) as S-Sequence_in_R2 by A15, A16, A21, Th67;

        (g /. 1) = ( SW-corner ( L~ z)) by FINSEQ_5: 15;

        then

         A34: ((g /. 1) `2 ) = ( S-bound ( L~ z)) by EUCLID: 52;

        ( len M) in ( dom M) & ( len g) = (( len M) + ( len <*( SW-corner ( L~ z))*>)) by FINSEQ_1: 22, FINSEQ_5: 6;

        then (g /. ( len g)) = (M /. ( len M)) by FINSEQ_4: 69;

        then

         A35: ((g /. ( len g)) `2 ) = ( N-bound ( L~ z)) by A10, A25, EUCLID: 52;

        (( LSeg ((M /. 1),( SW-corner ( L~ z)))) /\ ( L~ h)) c= (( LSeg ((M /. 1),( SW-corner ( L~ z)))) /\ ( L~ z)) by A13, A27, A20, A9, JORDAN4: 35, XBOOLE_1: 26;

        then

         A36: (( LSeg ((M /. 1),( SW-corner ( L~ z)))) /\ ( L~ h)) c= {(M /. 1)} by A16, A22, PSCOMP_1: 35;

        ( L~ g) = (( L~ M) \/ ( LSeg (( SW-corner ( L~ z)),(M /. 1)))) & (M /. 1) in ( L~ M) by A23, A19, JORDAN3: 1, SPPOL_2: 20;

        then

         A37: ( L~ g) misses ( L~ h) by A31, A36, ZFMISC_1: 125;

         <*( SW-corner ( L~ z))*> is_in_the_area_of z by Th28;

        then g is_in_the_area_of z by A24, Th24;

        then ( len g) >= 2 & g is_a_v.c._for z by A34, A35, TOPREAL1:def 8;

        hence contradiction by A30, A37, Th29;

      end;

    end;

    theorem :: SPRECT_2:76

    (z /. 1) = ( N-min ( L~ z)) implies (( W-min ( L~ z)) .. z) < ( len z)

    proof

      assume

       A1: (z /. 1) = ( N-min ( L~ z));

      

       A2: ( W-max ( L~ z)) in ( rng z) by Th44;

      

       A3: ( W-min ( L~ z)) in ( rng z) by Th43;

      per cases ;

        suppose ( N-min ( L~ z)) = ( W-max ( L~ z));

        then

         A4: (z /. ( len z)) = ( W-max ( L~ z)) by A1, FINSEQ_6:def 1;

        

         A5: (( W-min ( L~ z)) .. z) in ( dom z) by A3, FINSEQ_4: 20;

        then

         A6: (( W-min ( L~ z)) .. z) <= ( len z) by FINSEQ_3: 25;

        (z /. (( W-min ( L~ z)) .. z)) = (z . (( W-min ( L~ z)) .. z)) by A5, PARTFUN1:def 6

        .= ( W-min ( L~ z)) by A3, FINSEQ_4: 19;

        then (( W-min ( L~ z)) .. z) <> ( len z) by A4, Th58;

        hence thesis by A6, XXREAL_0: 1;

      end;

        suppose

         A7: ( N-min ( L~ z)) <> ( W-max ( L~ z));

        (( W-max ( L~ z)) .. z) in ( dom z) by A2, FINSEQ_4: 20;

        then (( W-max ( L~ z)) .. z) <= ( len z) by FINSEQ_3: 25;

        hence thesis by A1, A7, Th75, XXREAL_0: 2;

      end;

    end;

    theorem :: SPRECT_2:77

    (f /. 1) = ( N-min ( L~ f)) implies (( W-max ( L~ f)) .. f) < ( len f)

    proof

      assume

       A1: (f /. 1) = ( N-min ( L~ f));

      then

       A2: (f /. ( len f)) = ( N-min ( L~ f)) by FINSEQ_6:def 1;

      

       A3: ( W-max ( L~ f)) in ( rng f) by Th44;

      then (( W-max ( L~ f)) .. f) in ( dom f) by FINSEQ_4: 20;

      

      then

       A4: (f /. (( W-max ( L~ f)) .. f)) = (f . (( W-max ( L~ f)) .. f)) by PARTFUN1:def 6

      .= ( W-max ( L~ f)) by A3, FINSEQ_4: 19;

      per cases ;

        suppose ( N-min ( L~ f)) = ( W-max ( L~ f));

        then (( W-max ( L~ f)) .. f) = 1 by A1, FINSEQ_6: 43;

        hence thesis by GOBOARD7: 34, XXREAL_0: 2;

      end;

        suppose

         A5: ( N-min ( L~ f)) <> ( W-max ( L~ f));

        (( W-max ( L~ f)) .. f) <= ( len f) by A3, FINSEQ_4: 21;

        hence thesis by A2, A4, A5, XXREAL_0: 1;

      end;

    end;