sprect_4.miz



    begin

    reserve i,j,l for Nat;

    theorem :: SPRECT_4:1

    

     Th1: for f be S-Sequence_in_R2, Q be closed Subset of ( TOP-REAL 2) st ( L~ f) meets Q & not (f /. 1) in Q holds (( L~ ( R_Cut (f,( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q))))) /\ Q) = {( First_Point (( L~ f),(f /. 1),(f /. ( len f)),Q))}

    proof

      let f be S-Sequence_in_R2, Q be closed Subset of ( TOP-REAL 2) such that

       A1: ( L~ f) meets Q and

       A2: not (f /. 1) in Q;

      set p1 = (f /. 1), p2 = (f /. ( len f)), fp = ( First_Point (( L~ f),p1,p2,Q));

      

       A3: (( L~ f) /\ Q) is closed by TOPS_1: 8;

      ( len f) >= (1 + 1) by TOPREAL1:def 8;

      then

       A4: ( len f) > 1 by NAT_1: 13;

      then

       AA: 1 in ( dom f) by FINSEQ_3: 25;

      ( L~ f) is_an_arc_of (p1,p2) by TOPREAL1: 25;

      then

       A5: fp in (( L~ f) /\ Q) by A1, A3, JORDAN5C:def 1;

      then

       A6: fp in ( L~ f) by XBOOLE_0:def 4;

      then

       A7: 1 <= ( Index (fp,f)) by JORDAN3: 8;

      

       A8: ( Index (fp,f)) <= ( len f) by A6, JORDAN3: 8;

      then

       A9: ( Index (fp,f)) in ( dom f) by A7, FINSEQ_3: 25;

       A10:

      now

        assume not (( L~ ( R_Cut (f,fp))) /\ Q) c= {fp};

        then

        consider q be object such that

         A11: q in (( L~ ( R_Cut (f,fp))) /\ Q) and

         A12: not q in {fp} by TARSKI:def 3;

        reconsider q as Point of ( TOP-REAL 2) by A11;

        

         A13: q in ( L~ ( R_Cut (f,fp))) by A11, XBOOLE_0:def 4;

        

         A14: ( L~ ( R_Cut (f,fp))) c= ( L~ f) by A6, JORDAN3: 41;

        

         A15: q <> fp by A12, TARSKI:def 1;

        q in Q by A11, XBOOLE_0:def 4;

        then

         A16: LE (fp,q,( L~ f),p1,p2) by A3, A13, A14, JORDAN5C: 15;

        per cases ;

          suppose

           A17: fp = (f . 1);

          

           A18: ( len <*fp*>) = 1 by FINSEQ_1: 39;

          q in ( L~ <*fp*>) by A13, A17, JORDAN3:def 4;

          hence contradiction by A18, TOPREAL1: 22;

        end;

          suppose

           A19: fp <> (f . 1);

          set m = ( mid (f,1,( Index (fp,f))));

          

           A20: ( Index (fp,f)) < ( len f) by A6, JORDAN3: 8;

          ( len m) = ((( Index (fp,f)) -' 1) + 1) by A7, A8, JORDAN4: 8;

          then

           A21: m is non empty by CARD_1: 27;

          

           A22: fp in ( LSeg (f,( Index (fp,f)))) by A6, JORDAN3: 9;

          q in ( L~ (m ^ <*fp*>)) by A13, A19, JORDAN3:def 4;

          then

           A23: q in (( L~ m) \/ ( LSeg ((m /. ( len m)),fp))) by A21, SPPOL_2: 19;

          now

            per cases by A23, XBOOLE_0:def 3;

              suppose

               A24: q in ( L~ m);

               A25:

              now

                assume ( Index (fp,f)) <= 1;

                then ( Index (fp,f)) = 1 by A7, XXREAL_0: 1;

                then ( len m) = 1 by AA, JORDAN4: 15;

                hence contradiction by A24, TOPREAL1: 22;

              end;

              then

               A26: LE (q,(f /. ( Index (fp,f))),( L~ f),p1,p2) by A8, A24, SPRECT_3: 17;

              (f /. ( Index (fp,f))) in ( LSeg ((f /. ( Index (fp,f))),fp)) by RLTOPSP1: 68;

              then LE ((f /. ( Index (fp,f))),fp,( L~ f),p1,p2) by A20, A22, A25, SPRECT_3: 23;

              then LE (q,fp,( L~ f),p1,p2) by A26, JORDAN5C: 13;

              hence contradiction by A15, A16, JORDAN5C: 12, TOPREAL1: 25;

            end;

              suppose

               A27: q in ( LSeg ((m /. ( len m)),fp));

              ( len m) in ( dom m) by A21, FINSEQ_5: 6;

              

              then (m /. ( len m)) = (m . ( len m)) by PARTFUN1:def 6

              .= (f . ( Index (fp,f))) by A7, A8, JORDAN4: 10

              .= (f /. ( Index (fp,f))) by A9, PARTFUN1:def 6;

              then LE (q,fp,( L~ f),p1,p2) by A7, A20, A22, A27, SPRECT_3: 23;

              hence contradiction by A15, A16, JORDAN5C: 12, TOPREAL1: 25;

            end;

          end;

          hence contradiction;

        end;

      end;

      

       A28: fp in Q by A5, XBOOLE_0:def 4;

      1 in ( dom f) by A4, FINSEQ_3: 25;

      then fp <> (f . 1) by A2, A28, PARTFUN1:def 6;

      then fp in ( L~ ( R_Cut (f,fp))) by A6, JORDAN5B: 20;

      then fp in (( L~ ( R_Cut (f,fp))) /\ Q) by A28, XBOOLE_0:def 4;

      hence thesis by A10, ZFMISC_1: 33;

    end;

    theorem :: SPRECT_4:2

    for f be non empty FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st f is being_S-Seq & p = (f /. ( len f)) holds ( L~ ( L_Cut (f,p))) = {}

    proof

      let f be non empty FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2);

      assume that

       A1: f is being_S-Seq and

       A2: p = (f /. ( len f));

      ( len f) >= 2 by A1, TOPREAL1:def 8;

      then ( len f) >= 1 by XXREAL_0: 2;

      then ( len f) in ( dom f) by FINSEQ_3: 25;

      then p = (f . ( len f)) by A2, PARTFUN1:def 6;

      then ( L_Cut (f,p)) = <*p*> by A1, JORDAN5B: 17;

      then ( len ( L_Cut (f,p))) = 1 by FINSEQ_1: 39;

      hence thesis by TOPREAL1: 22;

    end;

    theorem :: SPRECT_4:3

    

     Th3: for f be S-Sequence_in_R2, p be Point of ( TOP-REAL 2), j st 1 <= j & j < ( len f) & p in ( L~ ( mid (f,j,( len f)))) holds LE ((f /. j),p,( L~ f),(f /. 1),(f /. ( len f)))

    proof

      let f be S-Sequence_in_R2, p be Point of ( TOP-REAL 2), j such that

       A1: 1 <= j and

       A2: j < ( len f) and

       A3: p in ( L~ ( mid (f,j,( len f))));

      consider i such that

       A4: 1 <= i and

       A5: (i + 1) <= ( len ( mid (f,j,( len f)))) and

       A6: p in ( LSeg (( mid (f,j,( len f))),i)) by A3, SPPOL_2: 13;

      

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

      then i <= (( len f) -' j) by A5, XREAL_1: 6;

      then

       A8: (i + j) <= ( len f) by A2, NAT_D: 54;

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

      then

       A9: (((j + i) -' 1) + 1) <= ( len f) by A4, A8, XREAL_1: 235, XXREAL_0: 2;

      (1 + 1) <= (j + i) by A1, A4, XREAL_1: 7;

      then

       A10: 1 <= ((j + i) -' 1) by NAT_D: 49;

      (j + 1) <= (j + i) by A4, XREAL_1: 6;

      then

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

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

      then ( len f) >= ((j + i) -' 1) by A9, XXREAL_0: 2;

      then

       A12: LE ((f /. j),(f /. ((j + i) -' 1)),( L~ f),(f /. 1),(f /. ( len f))) by A1, A11, JORDAN5C: 24;

      i < ((( len f) -' j) + 1) by A5, A7, NAT_1: 13;

      then p in ( LSeg (f,((j + i) -' 1))) by A1, A2, A4, A6, JORDAN4: 19;

      then LE ((f /. ((j + i) -' 1)),p,( L~ f),(f /. 1),(f /. ( len f))) by A10, A9, JORDAN5C: 25;

      hence thesis by A12, JORDAN5C: 13;

    end;

    theorem :: SPRECT_4:4

    

     Th4: for f be S-Sequence_in_R2, p,q be Point of ( TOP-REAL 2), j st 1 <= j & j < ( len f) & p in ( LSeg (f,j)) & q in ( LSeg (p,(f /. (j + 1)))) holds LE (p,q,( L~ f),(f /. 1),(f /. ( len f)))

    proof

      let f be S-Sequence_in_R2, p,q be Point of ( TOP-REAL 2), j such that

       A1: 1 <= j and

       A2: j < ( len f) and

       A3: p in ( LSeg (f,j)) and

       A4: q in ( LSeg (p,(f /. (j + 1))));

      

       A5: (j + 1) <= ( len f) by A2, NAT_1: 13;

      then

       A6: ( LSeg (f,j)) = ( LSeg ((f /. j),(f /. (j + 1)))) by A1, TOPREAL1:def 3;

      

       A7: (f /. (j + 1)) in ( LSeg (f,j)) by A1, A5, TOPREAL1: 21;

      then

       A8: ( LSeg (p,(f /. (j + 1)))) c= ( LSeg (f,j)) by A3, A6, TOPREAL1: 6;

      then

       A9: q in ( LSeg (f,j)) by A4;

      

       A10: ( LSeg (f,j)) c= ( L~ f) by TOPREAL3: 19;

      per cases ;

        suppose p = q;

        hence thesis by A3, A10, JORDAN5C: 9;

      end;

        suppose

         A11: q <> p;

        for i,j be Nat st p in ( LSeg (f,i)) & q in ( LSeg (f,j)) & 1 <= i & (i + 1) <= ( len f) & 1 <= j & (j + 1) <= ( len f) holds i <= j & (i = j implies LE (p,q,(f /. i),(f /. (i + 1))))

        proof

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

          then

           A12: (j + 1) in ( dom f) by A5, FINSEQ_3: 25;

          let i1,i2 be Nat such that

           A13: p in ( LSeg (f,i1)) and

           A14: q in ( LSeg (f,i2)) and 1 <= i1 and

           A15: (i1 + 1) <= ( len f) and

           A16: 1 <= i2 and (i2 + 1) <= ( len f);

          

           A17: p in (( LSeg (f,i1)) /\ ( LSeg (f,j))) by A3, A13, XBOOLE_0:def 4;

          then

           A18: ( LSeg (f,i1)) meets ( LSeg (f,j)) by XBOOLE_0: 4;

          then

           A19: (i1 + 1) >= j by TOPREAL1:def 7;

           A20:

          now

            

             A21: (j + (1 + 1)) = ((j + 1) + 1);

            assume (j + 1) = i1;

            then p in {(f /. (j + 1))} by A1, A15, A17, A21, TOPREAL1:def 6;

            then p = (f /. (j + 1)) by TARSKI:def 1;

            then q in {p} by A4, RLTOPSP1: 70;

            hence contradiction by A11, TARSKI:def 1;

          end;

           A22:

          now

            assume that

             A23: (i2 + 1) > j and

             A24: (j + 1) > i2;

            

             A25: j <= i2 by A23, NAT_1: 13;

            i2 <= j by A24, NAT_1: 13;

            hence i2 = j by A25, XXREAL_0: 1;

          end;

           A26:

          now

            assume that

             A27: (i1 + 1) > j and

             A28: (j + 1) > i1;

            

             A29: j <= i1 by A27, NAT_1: 13;

            i1 <= j by A28, NAT_1: 13;

            hence i1 = j by A29, XXREAL_0: 1;

          end;

          

           A30: q in (( LSeg (f,i2)) /\ ( LSeg (f,j))) by A4, A8, A14, XBOOLE_0:def 4;

          then

           A31: ( LSeg (f,i2)) meets ( LSeg (f,j)) by XBOOLE_0: 4;

          then

           A32: (j + 1) >= i2 by TOPREAL1:def 7;

          

           A33: j in ( dom f) by A1, A2, FINSEQ_3: 25;

           A34:

          now

            assume (f /. (j + 1)) = (f /. j);

            then j = (j + 1) by A12, A33, PARTFUN2: 10;

            hence contradiction;

          end;

           A35:

          now

            

             A36: (i2 + (1 + 1)) = ((i2 + 1) + 1);

            assume (i2 + 1) = j;

            then q in {(f /. j)} by A5, A16, A30, A36, TOPREAL1:def 6;

            then q = (f /. j) by TARSKI:def 1;

            hence contradiction by A3, A4, A6, A7, A11, A34, SPPOL_1: 7, TOPREAL1: 6;

          end;

          (i2 + 1) >= j by A31, TOPREAL1:def 7;

          then (i2 + 1) = j or i2 = j or (j + 1) = i2 by A22, A32, XXREAL_0: 1;

          then

           A37: i2 >= j by A35, NAT_1: 11;

          

           A38: (j + 1) >= i1 by A18, TOPREAL1:def 7;

          then (i1 + 1) = j or i1 = j by A26, A19, A20, XXREAL_0: 1;

          then i1 <= j by NAT_1: 11;

          hence i1 <= i2 by A37, XXREAL_0: 2;

          assume

           A39: i1 = i2;

           not p in ( LSeg (q,(f /. (j + 1)))) by A4, A11, SPRECT_3: 6;

          then not LE (q,p,(f /. j),(f /. (j + 1))) by JORDAN3: 30;

          then LT (p,q,(f /. j),(f /. (j + 1))) by A3, A6, A14, A26, A19, A38, A20, A34, A35, A39, JORDAN3: 28, XXREAL_0: 1;

          hence thesis by A26, A19, A38, A20, A35, A39, JORDAN3:def 6, XXREAL_0: 1;

        end;

        hence thesis by A3, A9, A10, A11, JORDAN5C: 30;

      end;

    end;

    theorem :: SPRECT_4:5

    

     Th5: for f be S-Sequence_in_R2, Q be closed Subset of ( TOP-REAL 2) st ( L~ f) meets Q & not (f /. ( len f)) in Q holds (( L~ ( L_Cut (f,( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q))))) /\ Q) = {( Last_Point (( L~ f),(f /. 1),(f /. ( len f)),Q))}

    proof

      let f be S-Sequence_in_R2, Q be closed Subset of ( TOP-REAL 2) such that

       A1: ( L~ f) meets Q and

       A2: not (f /. ( len f)) in Q;

      set p1 = (f /. 1), p2 = (f /. ( len f)), lp = ( Last_Point (( L~ f),p1,p2,Q));

      

       A3: (( L~ f) /\ Q) is closed by TOPS_1: 8;

      ( len f) >= (1 + 1) by TOPREAL1:def 8;

      then

       A4: ( len f) > 1 by NAT_1: 13;

      then

       AA: ( len f) in ( dom f) by FINSEQ_3: 25;

      ( L~ f) is_an_arc_of (p1,p2) by TOPREAL1: 25;

      then

       A5: lp in (( L~ f) /\ Q) by A1, A3, JORDAN5C:def 2;

      then

       A6: lp in ( L~ f) by XBOOLE_0:def 4;

      then

       A7: 1 <= ( Index (lp,f)) by JORDAN3: 8;

       A8:

      now

        set m = ( mid (f,(( Index (lp,f)) + 1),( len f)));

        assume not (( L~ ( L_Cut (f,lp))) /\ Q) c= {lp};

        then

        consider q be object such that

         A9: q in (( L~ ( L_Cut (f,lp))) /\ Q) and

         A10: not q in {lp} by TARSKI:def 3;

        reconsider q as Point of ( TOP-REAL 2) by A9;

        

         A11: q in ( L~ ( L_Cut (f,lp))) by A9, XBOOLE_0:def 4;

        

         A12: ( L~ ( L_Cut (f,lp))) c= ( L~ f) by A6, JORDAN3: 42;

        

         A13: ( Index (lp,f)) < ( len f) by A6, JORDAN3: 8;

        then

         A14: (( Index (lp,f)) + 1) <= ( len f) by NAT_1: 13;

        

         A15: 1 <= (( Index (lp,f)) + 1) by NAT_1: 11;

        then ( len m) = ((( len f) -' (( Index (lp,f)) + 1)) + 1) by A14, JORDAN4: 8;

        then

         A16: m is non empty by CARD_1: 27;

        

         A17: q <> lp by A10, TARSKI:def 1;

        q in Q by A9, XBOOLE_0:def 4;

        then

         A18: LE (q,lp,( L~ f),p1,p2) by A3, A11, A12, JORDAN5C: 16;

        per cases ;

          suppose lp = (f . (( Index (lp,f)) + 1));

          then

           A19: q in ( L~ m) by A11, JORDAN3:def 3;

          now

            assume (( Index (lp,f)) + 1) >= ( len f);

            then (( Index (lp,f)) + 1) = ( len f) by A14, XXREAL_0: 1;

            then ( len m) = 1 by AA, JORDAN4: 15;

            hence contradiction by A19, TOPREAL1: 22;

          end;

          then

           A20: LE ((f /. (( Index (lp,f)) + 1)),q,( L~ f),(f /. 1),(f /. ( len f))) by A19, Th3, NAT_1: 11;

          

           A21: (f /. (( Index (lp,f)) + 1)) in ( LSeg (lp,(f /. (( Index (lp,f)) + 1)))) by RLTOPSP1: 68;

          lp in ( LSeg (f,( Index (lp,f)))) by A6, JORDAN3: 9;

          then LE (lp,(f /. (( Index (lp,f)) + 1)),( L~ f),p1,p2) by A7, A13, A21, Th4;

          then LE (lp,q,( L~ f),p1,p2) by A20, JORDAN5C: 13;

          hence contradiction by A17, A18, JORDAN5C: 12, TOPREAL1: 25;

        end;

          suppose

           A22: lp <> (f . (( Index (lp,f)) + 1));

          

           A23: lp in ( LSeg (f,( Index (lp,f)))) by A6, JORDAN3: 9;

          1 <= (( Index (lp,f)) + 1) by NAT_1: 11;

          then

           A24: (( Index (lp,f)) + 1) in ( dom f) by A14, FINSEQ_3: 25;

          q in ( L~ ( <*lp*> ^ m)) by A11, A22, JORDAN3:def 3;

          then

           A25: q in (( L~ m) \/ ( LSeg ((m /. 1),lp))) by A16, SPPOL_2: 20;

          now

            per cases by A25, XBOOLE_0:def 3;

              suppose

               A26: q in ( L~ m);

              now

                assume (( Index (lp,f)) + 1) >= ( len f);

                then (( Index (lp,f)) + 1) = ( len f) by A14, XXREAL_0: 1;

                then ( len m) = 1 by AA, JORDAN4: 15;

                hence contradiction by A26, TOPREAL1: 22;

              end;

              then

               A27: LE ((f /. (( Index (lp,f)) + 1)),q,( L~ f),(f /. 1),(f /. ( len f))) by A26, Th3, NAT_1: 11;

              (f /. (( Index (lp,f)) + 1)) in ( LSeg (lp,(f /. (( Index (lp,f)) + 1)))) by RLTOPSP1: 68;

              then LE (lp,(f /. (( Index (lp,f)) + 1)),( L~ f),p1,p2) by A7, A13, A23, Th4;

              then LE (lp,q,( L~ f),p1,p2) by A27, JORDAN5C: 13;

              hence contradiction by A17, A18, JORDAN5C: 12, TOPREAL1: 25;

            end;

              suppose

               A28: q in ( LSeg (lp,(m /. 1)));

              1 in ( dom m) by A16, FINSEQ_5: 6;

              

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

              .= (f . (( Index (lp,f)) + 1)) by A4, A14, A15, FINSEQ_6: 118

              .= (f /. (( Index (lp,f)) + 1)) by A24, PARTFUN1:def 6;

              then LE (lp,q,( L~ f),p1,p2) by A7, A13, A23, A28, Th4;

              hence contradiction by A17, A18, JORDAN5C: 12, TOPREAL1: 25;

            end;

          end;

          hence contradiction;

        end;

      end;

      

       A29: lp in Q by A5, XBOOLE_0:def 4;

      ( len f) in ( dom f) by A4, FINSEQ_3: 25;

      then lp <> (f . ( len f)) by A2, A29, PARTFUN1:def 6;

      then lp in ( L~ ( L_Cut (f,lp))) by A6, JORDAN5B: 19;

      then lp in (( L~ ( L_Cut (f,lp))) /\ Q) by A29, XBOOLE_0:def 4;

      hence thesis by A8, ZFMISC_1: 33;

    end;

    reserve q for Point of ( TOP-REAL 2);

    

     Lm1: for f be clockwise_oriented non constant standard special_circular_sequence st (f /. 1) = ( N-min ( L~ f)) holds ( LeftComp f) <> ( RightComp f)

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

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

      assume that

       A1: (f /. 1) = A and

       A2: ( LeftComp f) = ( RightComp f);

      

       A3: ( LeftComp ( SpStSeq ( L~ f))) c= ( LeftComp f) by A1, SPRECT_3: 41;

      consider i such that

       A4: 1 <= i and

       A5: i < ( len ( GoB f)) and

       A6: A = (( GoB f) * (i,( width ( GoB f)))) by SPRECT_3: 28;

      set w = ( width ( GoB f));

      

       A7: ( len f) > 4 by GOBOARD7: 34;

      

       A8: (1 + 1) <= ( len f) by GOBOARD7: 34, XXREAL_0: 2;

      

       A9: w > 1 by GOBOARD7: 33;

      then

       A10: ((w -' 1) + 1) = w by XREAL_1: 235;

      

       A11: [i, w] in ( Indices ( GoB f)) by A4, A5, A9, MATRIX_0: 30;

      

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

      

       A13: (i + 1) <= ( len ( GoB f)) by A5, NAT_1: 13;

      then

       A14: [(i + 1), w] in ( Indices ( GoB f)) by A9, A12, MATRIX_0: 30;

      

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

      

       A16: i in ( dom ( GoB f)) by A4, A5, FINSEQ_3: 25;

      then

       A17: (f /. (1 + 1)) = (( GoB f) * ((i + 1),w)) by A1, A6, SPRECT_3: 29;

      then

       A18: ( right_cell (f,1)) = ( cell (( GoB f),i,(w -' 1))) by A1, A6, A8, A10, A11, A14, GOBOARD5: 28;

      set z2 = ((1 / 2) * ((( GoB f) * (i,(w -' 1))) + (( GoB f) * ((i + 1),w)))), p1 = ((1 / 2) * ((( GoB f) * (i,w)) + (( GoB f) * ((i + 1),w)))), p2 = ((1 / 2) * ((( GoB f) * (i,(w -' 1))) + (( GoB f) * (i,w))));

      

       A19: 1 <= (w -' 1) by GOBOARD7: 33, NAT_D: 49;

      then

       A20: z2 in ( Int ( cell (( GoB f),i,(w -' 1)))) by A4, A10, A13, GOBOARD6: 31;

      

       A21: ( Int ( right_cell (f,1))) c= ( RightComp f) by A8, GOBOARD9: 25;

      

       A22: ( W-bound ( L~ ( SpStSeq ( L~ f)))) = ( W-bound ( L~ f)) by SPRECT_1: 58;

      

       A23: ( S-bound ( L~ ( SpStSeq ( L~ f)))) = ( S-bound ( L~ f)) by SPRECT_1: 59;

      

       A24: ( N-bound ( L~ ( SpStSeq ( L~ f)))) = ( N-bound ( L~ f)) by SPRECT_1: 60;

      

       A25: ( E-bound ( L~ ( SpStSeq ( L~ f)))) = ( E-bound ( L~ f)) by SPRECT_1: 61;

      

       A26: 1 < (i + 1) by A4, NAT_1: 13;

      

       A27: 1 <= ( len ( GoB f)) by A4, A5, XXREAL_0: 2;

      

       A28: (w -' 1) < w by A10, XREAL_1: 29;

      

       A29: z2 = ((1 / 2) * (A + (( GoB f) * ((i + 1),(w -' 1))))) by A4, A6, A10, A13, A19, GOBOARD7: 9;

      

      then

       A30: (z2 `1 ) = ((1 / 2) * ((A + (( GoB f) * ((i + 1),(w -' 1)))) `1 )) by TOPREAL3: 4

      .= ((1 / 2) * ((A `1 ) + ((( GoB f) * ((i + 1),(w -' 1))) `1 ))) by TOPREAL3: 2

      .= (((1 / 2) * (A `1 )) + ((1 / 2) * ((( GoB f) * ((i + 1),(w -' 1))) `1 )));

      

       A31: (z2 `2 ) = ((1 / 2) * ((A + (( GoB f) * ((i + 1),(w -' 1)))) `2 )) by A29, TOPREAL3: 4

      .= ((1 / 2) * ((A `2 ) + ((( GoB f) * ((i + 1),(w -' 1))) `2 ))) by TOPREAL3: 2

      .= ((1 / 2) * (( N-bound ( L~ f)) + ((( GoB f) * ((i + 1),(w -' 1))) `2 ))) by EUCLID: 52

      .= (((1 / 2) * ( N-bound ( L~ f))) + ((1 / 2) * ((( GoB f) * ((i + 1),(w -' 1))) `2 )));

      

       A32: (((1 / 2) * ( W-bound ( L~ f))) + ((1 / 2) * ( W-bound ( L~ f)))) = ( W-bound ( L~ f));

      

       A33: (((1 / 2) * ( S-bound ( L~ f))) + ((1 / 2) * ( S-bound ( L~ f)))) = ( S-bound ( L~ f));

      

       A34: (((1 / 2) * ( N-bound ( L~ f))) + ((1 / 2) * ( N-bound ( L~ f)))) = ( N-bound ( L~ f));

      

       A35: (((1 / 2) * ( E-bound ( L~ f))) + ((1 / 2) * ( E-bound ( L~ f)))) = ( E-bound ( L~ f));

      ( N-min ( L~ f)) in ( L~ f) by SPRECT_1: 11;

      then (A `1 ) >= ( W-bound ( L~ f)) by PSCOMP_1: 24;

      then

       A36: ((1 / 2) * (A `1 )) >= ((1 / 2) * ( W-bound ( L~ f))) by XREAL_1: 64;

      

       A37: ((( GoB f) * (1,(w -' 1))) `1 ) = ((( GoB f) * (1,1)) `1 ) by A19, A27, A28, GOBOARD5: 2;

      ((( GoB f) * ((i + 1),(w -' 1))) `1 ) > ((( GoB f) * (1,(w -' 1))) `1 ) by A13, A19, A26, A28, GOBOARD5: 3;

      then ((( GoB f) * ((i + 1),(w -' 1))) `1 ) > ( W-bound ( L~ f)) by A37, JORDAN5D: 37;

      then ((1 / 2) * ((( GoB f) * ((i + 1),(w -' 1))) `1 )) > ((1 / 2) * ( W-bound ( L~ f))) by XREAL_1: 68;

      then

       A38: ( W-bound ( L~ ( SpStSeq ( L~ f)))) < (z2 `1 ) by A22, A30, A32, A36, XREAL_1: 8;

      ( N-max ( L~ f)) in ( L~ f) by SPRECT_1: 11;

      then (( N-max ( L~ f)) `1 ) <= ( E-bound ( L~ f)) by PSCOMP_1: 24;

      then (A `1 ) < ( E-bound ( L~ f)) by SPRECT_2: 51, XXREAL_0: 2;

      then

       A39: ((1 / 2) * (A `1 )) < ((1 / 2) * ( E-bound ( L~ f))) by XREAL_1: 68;

      

       A40: ((( GoB f) * (( len ( GoB f)),(w -' 1))) `1 ) = ((( GoB f) * (( len ( GoB f)),1)) `1 ) by A19, A27, A28, GOBOARD5: 2;

      ((( GoB f) * ((i + 1),(w -' 1))) `1 ) <= ((( GoB f) * (( len ( GoB f)),(w -' 1))) `1 ) by A12, A13, A19, A28, SPRECT_3: 13;

      then ((( GoB f) * ((i + 1),(w -' 1))) `1 ) <= ( E-bound ( L~ f)) by A40, JORDAN5D: 39;

      then ((1 / 2) * ((( GoB f) * ((i + 1),(w -' 1))) `1 )) <= ((1 / 2) * ( E-bound ( L~ f))) by XREAL_1: 64;

      then

       A41: (z2 `1 ) < ( E-bound ( L~ ( SpStSeq ( L~ f)))) by A25, A30, A35, A39, XREAL_1: 8;

      

       A42: ((1 / 2) * ( N-bound ( L~ f))) > ((1 / 2) * ( S-bound ( L~ f))) by SPRECT_1: 32, XREAL_1: 68;

      

       A43: ((( GoB f) * ((i + 1),1)) `2 ) = ((( GoB f) * (1,1)) `2 ) by A9, A12, A13, GOBOARD5: 1;

      ((( GoB f) * ((i + 1),(w -' 1))) `2 ) >= ((( GoB f) * ((i + 1),1)) `2 ) by A12, A13, A19, A28, SPRECT_3: 12;

      then ((( GoB f) * ((i + 1),(w -' 1))) `2 ) >= ( S-bound ( L~ f)) by A43, JORDAN5D: 38;

      then ((1 / 2) * ((( GoB f) * ((i + 1),(w -' 1))) `2 )) >= ((1 / 2) * ( S-bound ( L~ f))) by XREAL_1: 64;

      then

       A44: ( S-bound ( L~ ( SpStSeq ( L~ f)))) < (z2 `2 ) by A23, A31, A33, A42, XREAL_1: 8;

      

       A45: ((( GoB f) * ((i + 1),w)) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A9, A12, A13, GOBOARD5: 1;

      ((( GoB f) * ((i + 1),(w -' 1))) `2 ) < ((( GoB f) * ((i + 1),w)) `2 ) by A12, A13, A19, A28, GOBOARD5: 4;

      then ((( GoB f) * ((i + 1),(w -' 1))) `2 ) < ( N-bound ( L~ f)) by A45, JORDAN5D: 40;

      then ((1 / 2) * ((( GoB f) * ((i + 1),(w -' 1))) `2 )) < ((1 / 2) * ( N-bound ( L~ f))) by XREAL_1: 68;

      then

       A46: (z2 `2 ) < ( N-bound ( L~ ( SpStSeq ( L~ f)))) by A24, A31, A34, XREAL_1: 6;

      ( RightComp ( SpStSeq ( L~ f))) = { q : ( W-bound ( L~ ( SpStSeq ( L~ f)))) < (q `1 ) & (q `1 ) < ( E-bound ( L~ ( SpStSeq ( L~ f)))) & ( S-bound ( L~ ( SpStSeq ( L~ f)))) < (q `2 ) & (q `2 ) < ( N-bound ( L~ ( SpStSeq ( L~ f)))) } by SPRECT_3: 37;

      then

       A47: z2 in ( RightComp ( SpStSeq ( L~ f))) by A38, A41, A44, A46;

      consider z1 be object such that

       A48: z1 in ( LeftComp ( SpStSeq ( L~ f))) by XBOOLE_0:def 1;

      ( LeftComp ( SpStSeq ( L~ f))) misses ( RightComp ( SpStSeq ( L~ f))) by SPRECT_1: 88;

      then

       A49: z1 <> z2 by A47, A48, XBOOLE_0: 3;

      reconsider z1 as Point of ( TOP-REAL 2) by A48;

      consider P be Subset of ( TOP-REAL 2) such that

       A50: P is_S-P_arc_joining (z1,z2) and

       A51: P c= ( RightComp f) by A2, A3, A18, A20, A21, A48, A49, TOPREAL4: 29;

      consider Red9 be FinSequence of ( TOP-REAL 2) such that

       A52: Red9 is being_S-Seq and

       A53: P = ( L~ Red9) and

       A54: z1 = (Red9 /. 1) and

       A55: z2 = (Red9 /. ( len Red9)) by A50, TOPREAL4:def 1;

      

       A56: ( L~ ( SpStSeq ( L~ f))) meets ( L~ Red9) by A47, A48, A52, A54, A55, SPRECT_3: 33;

      

       A57: 2 in ( dom f) by A8, FINSEQ_3: 25;

      

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

      

       A59: (( len f) -' 1) >= 1 by A8, NAT_D: 49;

      (( len f) -' 1) <= ( len f) by NAT_D: 44;

      then

       A60: (( len f) -' 1) in ( dom f) by A59, FINSEQ_3: 25;

      1 <= ( len f) by A58, FINSEQ_3: 25;

      then

       A61: ((( len f) -' 1) + 1) = ( len f) by XREAL_1: 235;

      then

       A62: (( len f) -' 1) < ( len f) by NAT_1: 13;

      

       A63: <*( NW-corner ( L~ f))*> is_in_the_area_of f by SPRECT_2: 26;

      

       A64: (w -' 1) < ( width ( GoB f)) by A10, NAT_1: 13;

      then ( Int ( cell (( GoB f),i,(w -' 1)))) misses ( L~ ( SpStSeq ( L~ f))) by A4, A5, A19, SPRECT_3: 55;

      then

       A65: not z2 in ( L~ ( SpStSeq ( L~ f))) by A20, XBOOLE_0: 3;

      

       A66: ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) c= ( L~ ( SpStSeq ( L~ f))) by SPRECT_3: 14;

      

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

      

       A68: ( NW-corner ( L~ f)) in ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) by RLTOPSP1: 68;

      

       A69: ( N-min ( L~ f)) in ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) by SPRECT_3: 15;

      then

       A70: ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) c= ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) by A68, TOPREAL1: 6;

      

       A71: ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) is horizontal by A70, SPRECT_1: 9;

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

      then

       A72: (( LSeg (f,1)) /\ ( LSeg (f,(1 + 1)))) = {(f /. (1 + 1))} by TOPREAL1:def 6;

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

      then (( len f) -' 1) >= (1 + 1) by NAT_D: 49;

      then ((( len f) -' 1) -' 1) >= 1 by NAT_D: 49;

      then

       A73: (( len f) -' 2) >= 1 by NAT_D: 45;

      

       A74: ((( len f) -' 2) + 1) = (((( len f) -' 1) -' 1) + 1) by NAT_D: 45

      .= (( len f) -' 1) by A59, XREAL_1: 235;

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

      then

       A75: (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (f,(( len f) -' 2)))) = {(f /. (( len f) -' 1))} by A73, A74, TOPREAL1:def 6;

      

       A76: (f /. 2) in ( N-most ( L~ f)) by A1, SPRECT_2: 30;

      ( N-most ( L~ f)) c= ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) by XBOOLE_1: 17;

      then

       A77: ( LSeg ((f /. 1),(f /. 2))) c= ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) by A1, A69, A76, TOPREAL1: 6;

      

       A78: ((( GoB f) * (i,(w -' 1))) `1 ) = ((( GoB f) * (i,1)) `1 ) by A4, A5, A19, A64, GOBOARD5: 2

      .= (A `1 ) by A4, A5, A6, A9, GOBOARD5: 2;

      

       A79: ((( GoB f) * ((i + 1),w)) `2 ) = ((( GoB f) * (1,w)) `2 ) by A9, A12, A13, GOBOARD5: 1

      .= (A `2 ) by A4, A5, A6, A9, GOBOARD5: 1;

      then

       A80: ((f /. 2) `2 ) = ( N-bound ( L~ f)) by A17, EUCLID: 52;

      

       A81: <*(( GoB f) * ((i + 1),w))*> is_in_the_area_of f by A9, A12, A13, SPRECT_3: 49;

       <*(( GoB f) * (i,(w -' 1)))*> is_in_the_area_of f by A4, A5, A19, A64, SPRECT_3: 49;

      then <*(( GoB f) * (i,(w -' 1))), (( GoB f) * ((i + 1),w))*> is_in_the_area_of f by A81, SPRECT_3: 42;

      then <*z2*> is_in_the_area_of f by SPRECT_3: 50;

      then

       A82: <*z2*> is_in_the_area_of ( SpStSeq ( L~ f)) by SPRECT_3: 53;

      

       A83: (( GoB f) * (i,(w -' 1))) = (f /. (( len f) -' 1)) by A1, A6, A16, SPRECT_3: 29;

      then ( LSeg (A,(f /. (( len f) -' 1)))) is vertical by A78, SPPOL_1: 16;

      then

       A84: (( LSeg (A,(f /. (( len f) -' 1)))) /\ ( LSeg (( NW-corner ( L~ f)),A))) = {A} by A70, SPRECT_1: 9, SPRECT_3: 10;

      

       A85: (( NW-corner ( L~ f)) `2 ) = (A `2 ) by PSCOMP_1: 37;

      

       A86: (( NW-corner ( L~ f)) `1 ) <= (A `1 ) by PSCOMP_1: 38;

      (A `1 ) <= ((f /. 2) `1 ) by A76, PSCOMP_1: 39;

      then A in ( LSeg (( NW-corner ( L~ f)),(f /. 2))) by A17, A79, A85, A86, GOBOARD7: 8;

      then

       A87: (( LSeg (A,(f /. 2))) /\ ( LSeg (( NW-corner ( L~ f)),A))) = {A} by TOPREAL1: 8;

      ((( GoB f) * (i,w)) `2 ) = ((( GoB f) * (1,w)) `2 ) by A4, A5, A9, GOBOARD5: 1

      .= ((( GoB f) * ((i + 1),w)) `2 ) by A9, A12, A13, GOBOARD5: 1;

      

      then (((( GoB f) * (i,(w -' 1))) + (( GoB f) * (i,w))) `2 ) = (((( GoB f) * (i,(w -' 1))) `2 ) + ((( GoB f) * ((i + 1),w)) `2 )) by TOPREAL3: 2

      .= (((( GoB f) * (i,(w -' 1))) + (( GoB f) * ((i + 1),w))) `2 ) by TOPREAL3: 2;

      

      then (p2 `2 ) = ((1 / 2) * (((( GoB f) * (i,(w -' 1))) + (( GoB f) * ((i + 1),w))) `2 )) by TOPREAL3: 4

      .= (z2 `2 ) by TOPREAL3: 4;

      then

       A88: ( LSeg (p2,z2)) is horizontal by SPPOL_1: 15;

      

       A89: (f /. (( len f) -' 1)) in ( LSeg ((f /. (( len f) -' 1)),(f /. ( len f)))) by RLTOPSP1: 68;

      

       A90: (( GoB f) * (i,w)) = (f /. ( len f)) by A1, A6, FINSEQ_6:def 1;

      p2 = (((1 / 2) * (( GoB f) * (i,(w -' 1)))) + ((1 - (1 / 2)) * (( GoB f) * (i,w)))) by RLVECT_1:def 5;

      then

       A91: p2 in ( LSeg ((f /. (( len f) -' 1)),(f /. ( len f)))) by A83, A90;

      then

       A92: ( LSeg (p2,(f /. (( len f) -' 1)))) c= ( LSeg ((f /. (( len f) -' 1)),(f /. ( len f)))) by A89, TOPREAL1: 6;

      ( LSeg ((f /. (( len f) -' 1)),(f /. ( len f)))) = ( LSeg (f,(( len f) -' 1))) by A59, A61, TOPREAL1:def 3;

      then

       A93: ( LSeg ((f /. (( len f) -' 1)),(f /. ( len f)))) c= ( L~ f) by TOPREAL3: 19;

      then

       A94: ( LSeg (p2,(f /. (( len f) -' 1)))) c= ( L~ f) by A92, XBOOLE_1: 1;

      

       A95: ( LSeg (p2,(f /. (( len f) -' 1)))) c= ( LSeg (f,(( len f) -' 1))) by A59, A61, A92, TOPREAL1:def 3;

      

       A96: (p2 `1 ) = ((1 / 2) * (((( GoB f) * (i,(w -' 1))) + A) `1 )) by A6, TOPREAL3: 4

      .= ((1 / 2) * ((A `1 ) + (A `1 ))) by A78, TOPREAL3: 2

      .= (( N-min ( L~ f)) `1 );

      then

       A97: ( LSeg (p2,(f /. (( len f) -' 1)))) is vertical by A78, A83, SPPOL_1: 16;

      

       A98: p2 in ( LSeg (p2,(f /. (( len f) -' 1)))) by RLTOPSP1: 68;

      then

       A99: p2 in ( L~ f) by A94;

       A100:

      now

        assume p2 = A;

        then (f /. (( len f) -' 1)) = (f /. ( len f)) by A1, A6, A67, A83, SPRECT_3: 5;

        hence contradiction by A58, A60, A61, GOBOARD7: 29;

      end;

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

      then

       A101: (1 + 1) <= (( len f) -' 1) by NAT_D: 49;

      then

       A102: 1 <= ((( len f) -' 1) -' 1) by NAT_D: 49;

      

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

      

       A104: (((( len f) -' 1) -' 1) + 2) = ((( len f) -' 2) + 2) by NAT_D: 45

      .= ( len f) by A7, XREAL_1: 235, XXREAL_0: 2;

      

       A105: for i, j st 1 <= i & i <= j & j < (( len f) -' 1) holds ( L~ ( mid (f,i,j))) misses ( LSeg (p2,(f /. (( len f) -' 1))))

      proof

        let l, j such that

         A106: 1 <= l and

         A107: l <= j and

         A108: j < (( len f) -' 1);

        assume ( L~ ( mid (f,l,j))) meets ( LSeg (p2,(f /. (( len f) -' 1))));

        then (( L~ ( mid (f,l,j))) /\ ( LSeg (p2,(f /. (( len f) -' 1))))) <> {} by XBOOLE_0:def 7;

        then

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

         A109: p in (( L~ ( mid (f,l,j))) /\ ( LSeg (p2,(f /. (( len f) -' 1))))) by SUBSET_1: 4;

        p in ( L~ ( mid (f,l,j))) by A109, XBOOLE_0:def 4;

        then

        consider ii be Nat such that

         A110: 1 <= ii and

         A111: (ii + 1) <= ( len ( mid (f,l,j))) and

         A112: p in ( LSeg (( mid (f,l,j)),ii)) by SPPOL_2: 13;

        (( len f) -' 1) > l by A107, A108, XXREAL_0: 2;

        then (( len f) -' 1) > 1 by A106, XXREAL_0: 2;

        then

         A113: (( len f) -' 1) < ( len f) by NAT_D: 51;

        then

         A114: j < ( len f) by A108, XXREAL_0: 2;

        then ( len ( mid (f,l,j))) = ((j -' l) + 1) by A106, A107, JORDAN4: 8;

        then

         A115: ii < ((j -' l) + 1) by A111, NAT_1: 13;

        set k = ((ii + l) -' 1);

        

         A116: p in ( LSeg (p2,(f /. (( len f) -' 1)))) by A109, XBOOLE_0:def 4;

        per cases by A107, XXREAL_0: 1;

          suppose

           AB: l = j;

          then j in ( dom f) by A106, A114, FINSEQ_3: 25;

          then ( len ( mid (f,l,j))) = 1 by AB, JORDAN4: 15;

          then ( L~ ( mid (f,l,j))) = {} by TOPREAL1: 22;

          hence thesis by A112, SPPOL_2: 17;

        end;

          suppose

           A117: l < j;

          

           A118: (ii + 1) >= (1 + 1) by A110, XREAL_1: 6;

          (ii + l) >= (ii + 1) by A106, XREAL_1: 6;

          then

           A119: (ii + l) >= (1 + 1) by A118, XXREAL_0: 2;

          then

           A120: k >= 1 by NAT_D: 49;

          

           A121: (ii + l) >= 1 by A119, XXREAL_0: 2;

           A122:

          now

            assume (k + 1) >= (( len f) -' 1);

            then k >= ((( len f) -' 1) -' 1) by NAT_D: 53;

            then

             A123: (ii + l) >= (( len f) -' 1) by A121, NAT_D: 56;

            (ii + l) < (((j -' l) + 1) + l) by A115, XREAL_1: 6;

            then (ii + l) < (((j -' l) + l) + 1);

            then (ii + l) < (j + 1) by A117, XREAL_1: 235;

            then (( len f) -' 1) < (j + 1) by A123, XXREAL_0: 2;

            hence contradiction by A108, NAT_1: 13;

          end;

          

           A124: (( LSeg (f,1)) /\ ( LSeg (f,(( len f) -' 1)))) = {(f . 1)} by JORDAN4: 42

          .= {(f /. 1)} by A15, PARTFUN1:def 6;

          ( LSeg (( mid (f,l,j)),ii)) = ( LSeg (f,k)) by A106, A114, A110, A115, A117, JORDAN4: 19;

          then

           A125: p in (( LSeg (f,k)) /\ ( LSeg (f,(( len f) -' 1)))) by A95, A116, A112, XBOOLE_0:def 4;

          then ( LSeg (f,k)) meets ( LSeg (f,(( len f) -' 1))) by XBOOLE_0: 4;

          then k <= 1 by A113, A122, GOBOARD5:def 4;

          then k = 1 by A120, XXREAL_0: 1;

          then p = (f /. 1) by A125, A124, TARSKI:def 1;

          hence contradiction by A1, A67, A91, A100, A116, SPRECT_3: 6;

        end;

      end;

      

       A126: for j st 1 <= j & j < (( len f) -' 1) holds (( L~ ( mid (f,j,(( len f) -' 1)))) /\ ( LSeg (p2,(f /. (( len f) -' 1))))) = {(f /. (( len f) -' 1))}

      proof

        let j such that

         A127: 1 <= j and

         A128: j < (( len f) -' 1);

        

         A129: 1 <= (( len f) -' 1) by A127, A128, XXREAL_0: 2;

        

         A130: ((( len f) -' 1) -' 1) = (( len f) -' 2) by NAT_D: 45;

        then

         A131: ( L~ ( mid (f,j,(( len f) -' 1)))) = (( LSeg (f,(( len f) -' 2))) \/ ( L~ ( mid (f,j,(( len f) -' 2))))) by A127, A128, NAT_D: 35, SPRECT_3: 20;

        j <= (( len f) -' 2) by A128, A130, NAT_D: 49;

        then ( LSeg (p2,(f /. (( len f) -' 1)))) misses ( L~ ( mid (f,j,(( len f) -' 2)))) by A105, A127, A129, A130, JORDAN5B: 1;

        

        hence (( L~ ( mid (f,j,(( len f) -' 1)))) /\ ( LSeg (p2,(f /. (( len f) -' 1))))) = (( LSeg (f,(( len f) -' 2))) /\ ( LSeg (p2,(f /. (( len f) -' 1))))) by A131, XBOOLE_1: 78

        .= {(f /. (( len f) -' 1))} by A75, A95, RLTOPSP1: 68, ZFMISC_1: 124;

      end;

      

       A132: ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) misses ( LSeg ((f /. (( len f) -' 1)),p2))

      proof

        assume ( LSeg (( NW-corner ( L~ f)),A)) meets ( LSeg ((f /. (( len f) -' 1)),p2));

        then (( LSeg (p2,(f /. (( len f) -' 1)))) /\ ( LSeg (( NW-corner ( L~ f)),A))) <> {} by XBOOLE_0:def 7;

        then

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

         A133: p in (( LSeg (p2,(f /. (( len f) -' 1)))) /\ ( LSeg (( NW-corner ( L~ f)),A))) by SUBSET_1: 4;

        

         A134: p in ( LSeg (p2,(f /. (( len f) -' 1)))) by A133, XBOOLE_0:def 4;

        p in ( LSeg (( NW-corner ( L~ f)),A)) by A133, XBOOLE_0:def 4;

        then p in {A} by A1, A67, A84, A92, A134, XBOOLE_0:def 4;

        then p = A by TARSKI:def 1;

        hence contradiction by A1, A67, A91, A100, A134, SPRECT_3: 6;

      end;

      

       A135: (p2 `2 ) <> (A `2 ) by A96, A100, TOPREAL3: 6;

      set G = ( GoB f);

      

       A136: ( Int ( cell (( GoB f),i,(w -' 1)))) misses ( L~ f) by A5, A64, GOBOARD7: 12;

      (( L~ f) /\ (( Int ( cell (G,i,(w -' 1)))) \/ {p2})) = ((( L~ f) /\ ( Int ( cell (G,i,(w -' 1))))) \/ (( L~ f) /\ {p2})) by XBOOLE_1: 23

      .= ( {} \/ (( L~ f) /\ {p2})) by A136, XBOOLE_0:def 7

      .= (( L~ f) /\ {p2});

      then

       A137: (( LSeg (z2,p2)) /\ ( L~ f)) c= (( L~ f) /\ {p2}) by A4, A5, A10, A19, A64, GOBOARD6: 40, XBOOLE_1: 26;

      (( L~ f) /\ {p2}) c= {p2} by XBOOLE_1: 17;

      then

       A138: (( LSeg (z2,p2)) /\ ( L~ f)) c= {p2} by A137, XBOOLE_1: 1;

      

       A139: for i, j st 1 <= i & i < j & j < ( len f) holds ( L~ ( mid (f,i,j))) misses ( LSeg (z2,p2))

      proof

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

        then

         A140: (( len f) -' 1) >= 1 by NAT_D: 49;

        let l, j such that

         A141: 1 <= l and

         A142: l < j and

         A143: j < ( len f);

        assume ( L~ ( mid (f,l,j))) meets ( LSeg (z2,p2));

        then (( L~ ( mid (f,l,j))) /\ ( LSeg (z2,p2))) <> {} by XBOOLE_0:def 7;

        then

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

         A144: p in (( L~ ( mid (f,l,j))) /\ ( LSeg (z2,p2))) by SUBSET_1: 4;

        p in ( L~ ( mid (f,l,j))) by A144, XBOOLE_0:def 4;

        then

        consider ii be Nat such that

         A145: 1 <= ii and

         A146: (ii + 1) <= ( len ( mid (f,l,j))) and

         A147: p in ( LSeg (( mid (f,l,j)),ii)) by SPPOL_2: 13;

        

         A148: ( len ( mid (f,l,j))) = ((j -' l) + 1) by A141, A142, A143, JORDAN4: 8;

        then ii < ((j -' l) + 1) by A146, NAT_1: 13;

        then

         A149: p in ( LSeg (f,((ii + l) -' 1))) by A141, A142, A143, A145, A147, JORDAN4: 19;

        set k = ((ii + l) -' 1);

        

         A150: (ii + 1) >= (1 + 1) by A145, XREAL_1: 6;

        (( LSeg (f,k)) /\ ( LSeg (z2,p2))) c= (( L~ f) /\ ( LSeg (z2,p2))) by TOPREAL3: 19, XBOOLE_1: 26;

        then

         A151: (( LSeg (f,k)) /\ ( LSeg (z2,p2))) c= {p2} by A138, XBOOLE_1: 1;

        p in ( LSeg (z2,p2)) by A144, XBOOLE_0:def 4;

        then p in (( LSeg (f,((ii + l) -' 1))) /\ ( LSeg (z2,p2))) by A149, XBOOLE_0:def 4;

        then p = p2 by A151, TARSKI:def 1;

        then p2 in (( LSeg (f,k)) /\ ( LSeg ((f /. (( len f) -' 1)),(f /. ( len f))))) by A91, A149, XBOOLE_0:def 4;

        then

         A152: p2 in (( LSeg (f,k)) /\ ( LSeg (f,(( len f) -' 1)))) by A61, A140, TOPREAL1:def 3;

        then

         A153: ( LSeg (f,k)) meets ( LSeg (f,(( len f) -' 1))) by XBOOLE_0: 4;

        (ii + l) >= (ii + 1) by A141, XREAL_1: 6;

        then (ii + l) >= (1 + 1) by A150, XXREAL_0: 2;

        then

         A154: k >= 1 by NAT_D: 49;

        per cases by A62, A153, GOBOARD5:def 4;

          suppose

           A155: k <= 1;

          

           A156: (( LSeg (f,1)) /\ ( LSeg (f,(( len f) -' 1)))) = {(f . 1)} by JORDAN4: 42

          .= {(f /. 1)} by A15, PARTFUN1:def 6;

          k = 1 by A154, A155, XXREAL_0: 1;

          hence contradiction by A1, A100, A152, A156, TARSKI:def 1;

        end;

          suppose

           A157: (k + 1) >= (( len f) -' 1);

          ii <= (j -' l) by A146, A148, XREAL_1: 6;

          then (ii + l) <= j by A142, NAT_D: 54;

          then

           A158: (ii + l) < ( len f) by A143, XXREAL_0: 2;

          (ii + l) >= l by NAT_1: 11;

          then (ii + l) >= 1 by A141, XXREAL_0: 2;

          then ((ii + l) -' 1) < (( len f) -' 1) by A158, NAT_D: 56;

          then

           A159: ((ii + l) -' 1) <= ((( len f) -' 1) -' 1) by NAT_D: 49;

          k >= ((( len f) -' 1) -' 1) by A157, NAT_D: 53;

          then k = ((( len f) -' 1) -' 1) by A159, XXREAL_0: 1;

          then p2 in {(f /. (( len f) -' 1))} by A102, A103, A104, A152, TOPREAL1:def 6;

          then p2 = (f /. (( len f) -' 1)) by TARSKI:def 1;

          hence contradiction by A6, A83, A100, SPRECT_3: 5;

        end;

      end;

      

       A160: <*p2*> is_in_the_area_of f by A94, A98, SPRECT_2: 21, SPRECT_3: 46;

      then

       A161: <*p2*> is_in_the_area_of ( SpStSeq ( L~ f)) by SPRECT_3: 53;

       <*p2, z2*> = ( <*p2*> ^ <*z2*>) by FINSEQ_1:def 9;

      then

       A162: (( L~ ( SpStSeq ( L~ f))) /\ ( LSeg (p2,z2))) c= {p2} by A65, A82, A161, SPRECT_2: 24, SPRECT_3: 47;

      ((( GoB f) * (i,(w -' 1))) `1 ) = ((( GoB f) * (i,1)) `1 ) by A4, A5, A19, GOBOARD5: 2, NAT_D: 35

      .= ((( GoB f) * (i,w)) `1 ) by A4, A5, A9, GOBOARD5: 2;

      

      then (((( GoB f) * (i,w)) + (( GoB f) * ((i + 1),w))) `1 ) = (((( GoB f) * (i,(w -' 1))) `1 ) + ((( GoB f) * ((i + 1),w)) `1 )) by TOPREAL3: 2

      .= (((( GoB f) * (i,(w -' 1))) + (( GoB f) * ((i + 1),w))) `1 ) by TOPREAL3: 2;

      

      then (p1 `1 ) = ((1 / 2) * (((( GoB f) * (i,(w -' 1))) + (( GoB f) * ((i + 1),w))) `1 )) by TOPREAL3: 4

      .= (z2 `1 ) by TOPREAL3: 4;

      then

       A163: ( LSeg (p1,z2)) is vertical by SPPOL_1: 16;

      

       A164: (f /. 2) in ( LSeg ((f /. 1),(f /. (1 + 1)))) by RLTOPSP1: 68;

      p1 = (((1 / 2) * (( GoB f) * (i,w))) + ((1 - (1 / 2)) * (( GoB f) * ((i + 1),w)))) by RLVECT_1:def 5;

      then

       A165: p1 in ( LSeg ((f /. 1),(f /. 2))) by A1, A6, A17;

      then

       A166: ( LSeg (p1,(f /. 2))) c= ( LSeg ((f /. 1),(f /. 2))) by A164, TOPREAL1: 6;

      

       A167: ( LSeg ((f /. 1),(f /. (1 + 1)))) = ( LSeg (f,1)) by A8, TOPREAL1:def 3;

      then

       A168: ( LSeg ((f /. 1),(f /. 2))) c= ( L~ f) by TOPREAL3: 19;

      then

       A169: ( LSeg (p1,(f /. 2))) c= ( L~ f) by A166, XBOOLE_1: 1;

      

       A170: (p1 `2 ) = ((1 / 2) * ((A + (( GoB f) * ((i + 1),w))) `2 )) by A6, TOPREAL3: 4

      .= ((1 / 2) * ((A `2 ) + (A `2 ))) by A79, TOPREAL3: 2

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

      

       A171: p1 in ( LSeg (p1,(f /. 2))) by RLTOPSP1: 68;

      

       A172: p1 <> A by A1, A6, A15, A17, A57, GOBOARD7: 29, SPRECT_3: 5;

      

       A173: for i, j st 2 < i & i <= j & j <= ( len f) holds ( L~ ( mid (f,i,j))) misses ( LSeg (p1,(f /. 2)))

      proof

        let l, j such that

         A174: 2 < l and

         A175: l <= j and

         A176: j <= ( len f);

        assume ( L~ ( mid (f,l,j))) meets ( LSeg (p1,(f /. 2)));

        then (( L~ ( mid (f,l,j))) /\ ( LSeg (p1,(f /. 2)))) <> {} by XBOOLE_0:def 7;

        then

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

         A177: p in (( L~ ( mid (f,l,j))) /\ ( LSeg (p1,(f /. 2)))) by SUBSET_1: 4;

        

         A178: p in ( LSeg (p1,(f /. 2))) by A177, XBOOLE_0:def 4;

        p in ( L~ ( mid (f,l,j))) by A177, XBOOLE_0:def 4;

        then

        consider ii be Nat such that

         A179: 1 <= ii and

         A180: (ii + 1) <= ( len ( mid (f,l,j))) and

         A181: p in ( LSeg (( mid (f,l,j)),ii)) by SPPOL_2: 13;

        

         A182: 1 < l by A174, XXREAL_0: 2;

        then

         A183: ( len ( mid (f,l,j))) = ((j -' l) + 1) by A175, A176, JORDAN4: 8;

        then

         A184: ii < ((j -' l) + 1) by A180, NAT_1: 13;

        set k = ((ii + l) -' 1);

        

         A185: (ii + 2) >= (1 + 2) by A179, XREAL_1: 6;

        (ii + l) > (ii + 2) by A174, XREAL_1: 6;

        then (ii + l) > (1 + 2) by A185, XXREAL_0: 2;

        then

         A186: k > (1 + 1) by NAT_D: 52;

        per cases by A175, XXREAL_0: 1;

          suppose

           AB: l = j;

          then j in ( dom f) by A176, A182, FINSEQ_3: 25;

          then ( len ( mid (f,l,j))) = 1 by AB, JORDAN4: 15;

          then ( L~ ( mid (f,l,j))) = {} by TOPREAL1: 22;

          hence thesis by A181, SPPOL_2: 17;

        end;

          suppose

           A187: l < j;

          

           A188: (( LSeg (f,1)) /\ ( LSeg (f,(( len f) -' 1)))) = {(f . 1)} by JORDAN4: 42

          .= {(f /. 1)} by A15, PARTFUN1:def 6;

          ii <= (j -' l) by A180, A183, XREAL_1: 6;

          then (ii + l) <= j by A175, NAT_D: 54;

          then (ii + l) <= ( len f) by A176, XXREAL_0: 2;

          then

           A189: ((ii + l) -' 1) <= (( len f) -' 1) by NAT_D: 42;

          ( LSeg (( mid (f,l,j)),ii)) = ( LSeg (f,k)) by A176, A182, A179, A184, A187, JORDAN4: 19;

          then

           A190: p in (( LSeg (f,k)) /\ ( LSeg (f,1))) by A166, A167, A178, A181, XBOOLE_0:def 4;

          then ( LSeg (f,k)) meets ( LSeg (f,1)) by XBOOLE_0: 4;

          then (k + 1) >= ( len f) by A186, GOBOARD5:def 4;

          then k >= (( len f) -' 1) by NAT_D: 53;

          then k = (( len f) -' 1) by A189, XXREAL_0: 1;

          then p = (f /. 1) by A190, A188, TARSKI:def 1;

          hence contradiction by A1, A165, A172, A178, SPRECT_3: 6;

        end;

      end;

      

       A191: for j st 2 < j & j <= ( len f) holds (( L~ ( mid (f,2,j))) /\ ( LSeg (p1,(f /. 2)))) = {(f /. 2)}

      proof

        

         A192: (f /. 2) in ( LSeg (p1,(f /. 2))) by RLTOPSP1: 68;

        let j such that

         A193: 2 < j and

         A194: j <= ( len f);

        (2 + 1) <= j by A193, NAT_1: 13;

        then

         A195: ( LSeg (p1,(f /. 2))) misses ( L~ ( mid (f,(2 + 1),j))) by A173, A194;

        ( L~ ( mid (f,2,j))) = (( LSeg (f,2)) \/ ( L~ ( mid (f,(2 + 1),j)))) by A193, A194, SPRECT_3: 19;

        

        hence (( L~ ( mid (f,2,j))) /\ ( LSeg (p1,(f /. 2)))) = (( LSeg (f,2)) /\ ( LSeg (p1,(f /. 2)))) by A195, XBOOLE_1: 78

        .= {(f /. 2)} by A72, A164, A165, A167, A192, TOPREAL1: 6, ZFMISC_1: 124;

      end;

      

       A196: ( LSeg (p1,(f /. 2))) misses ( LSeg (( NW-corner ( L~ f)),A))

      proof

        assume ( LSeg (p1,(f /. 2))) meets ( LSeg (( NW-corner ( L~ f)),A));

        then (( LSeg (p1,(f /. 2))) /\ ( LSeg (( NW-corner ( L~ f)),A))) <> {} by XBOOLE_0:def 7;

        then

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

         A197: p in (( LSeg (p1,(f /. 2))) /\ ( LSeg (( NW-corner ( L~ f)),A))) by SUBSET_1: 4;

        

         A198: p in ( LSeg (p1,(f /. 2))) by A197, XBOOLE_0:def 4;

        p in ( LSeg (( NW-corner ( L~ f)),A)) by A197, XBOOLE_0:def 4;

        then p in {A} by A1, A87, A166, A198, XBOOLE_0:def 4;

        then p = A by TARSKI:def 1;

        hence contradiction by A1, A165, A172, A198, SPRECT_3: 6;

      end;

      

       A199: ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) misses ( LSeg (z2,p1))

      proof

        assume ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) meets ( LSeg (z2,p1));

        then (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( LSeg (z2,p1))) <> {} by XBOOLE_0:def 7;

        then

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

         A200: p in (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( LSeg (z2,p1))) by SUBSET_1: 4;

        

         A201: p in ( LSeg (z2,p1)) by A200, XBOOLE_0:def 4;

        

         A202: p in ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) by A200, XBOOLE_0:def 4;

        (( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) /\ ( LSeg (z2,p1))) = {p1} by A77, A163, A165, SPRECT_3: 11;

        then p in {p1} by A70, A202, A201, XBOOLE_0:def 4;

        then p1 in ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) by A202, TARSKI:def 1;

        then p1 in (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ f)) by A169, A171, XBOOLE_0:def 4;

        then p1 in {( N-min ( L~ f))} by PSCOMP_1: 43;

        hence contradiction by A172, TARSKI:def 1;

      end;

      

       A203: for i, j st 1 < i & i < j & j <= ( len f) holds ( L~ ( mid (f,i,j))) misses ( LSeg (z2,p1))

      proof

        

         A204: ( len f) >= 2 by GOBOARD7: 34, XXREAL_0: 2;

        

         A205: ( Int ( cell (( GoB f),i,(w -' 1)))) misses ( L~ f) by A5, A64, GOBOARD7: 12;

        

         A206: (( L~ f) /\ {p1}) c= {p1} by XBOOLE_1: 17;

        let l, j such that

         A207: 1 < l and

         A208: l < j and

         A209: j <= ( len f);

        assume ( L~ ( mid (f,l,j))) meets ( LSeg (z2,p1));

        then (( L~ ( mid (f,l,j))) /\ ( LSeg (z2,p1))) <> {} by XBOOLE_0:def 7;

        then

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

         A210: p in (( L~ ( mid (f,l,j))) /\ ( LSeg (z2,p1))) by SUBSET_1: 4;

        p in ( L~ ( mid (f,l,j))) by A210, XBOOLE_0:def 4;

        then

        consider ii be Nat such that

         A211: 1 <= ii and

         A212: (ii + 1) <= ( len ( mid (f,l,j))) and

         A213: p in ( LSeg (( mid (f,l,j)),ii)) by SPPOL_2: 13;

        

         A214: ( len ( mid (f,l,j))) = ((j -' l) + 1) by A207, A208, A209, JORDAN4: 8;

        then ii < ((j -' l) + 1) by A212, NAT_1: 13;

        then

         A215: p in ( LSeg (f,((ii + l) -' 1))) by A207, A208, A209, A211, A213, JORDAN4: 19;

        set k = ((ii + l) -' 1), G = ( GoB f);

        

         A216: (( LSeg (f,k)) /\ ( LSeg (z2,p1))) c= (( L~ f) /\ ( LSeg (z2,p1))) by TOPREAL3: 19, XBOOLE_1: 26;

        (( L~ f) /\ (( Int ( cell (G,i,(w -' 1)))) \/ {p1})) = ((( L~ f) /\ ( Int ( cell (G,i,(w -' 1))))) \/ (( L~ f) /\ {p1})) by XBOOLE_1: 23

        .= ( {} \/ (( L~ f) /\ {p1})) by A205, XBOOLE_0:def 7

        .= (( L~ f) /\ {p1});

        then (( LSeg (z2,p1)) /\ ( L~ f)) c= (( L~ f) /\ {p1}) by A4, A5, A10, A19, A64, GOBOARD6: 41, XBOOLE_1: 26;

        then (( LSeg (z2,p1)) /\ ( L~ f)) c= {p1} by A206, XBOOLE_1: 1;

        then

         A217: (( LSeg (f,k)) /\ ( LSeg (z2,p1))) c= {p1} by A216, XBOOLE_1: 1;

        p in ( LSeg (z2,p1)) by A210, XBOOLE_0:def 4;

        then p in (( LSeg (f,((ii + l) -' 1))) /\ ( LSeg (z2,p1))) by A215, XBOOLE_0:def 4;

        then p = p1 by A217, TARSKI:def 1;

        then p1 in (( LSeg (f,k)) /\ ( LSeg ((f /. 1),(f /. (1 + 1))))) by A165, A215, XBOOLE_0:def 4;

        then

         A218: p1 in (( LSeg (f,k)) /\ ( LSeg (f,1))) by A204, TOPREAL1:def 3;

        then ( LSeg (f,k)) meets ( LSeg (f,1)) by XBOOLE_0: 4;

        then

         A219: k <= (1 + 1) or (k + 1) >= ( len f) by GOBOARD5:def 4;

        

         A220: (ii + 1) >= (1 + 1) by A211, XREAL_1: 6;

        (ii + l) > (ii + 1) by A207, XREAL_1: 6;

        then (ii + l) > (1 + 1) by A220, XXREAL_0: 2;

        then

         A221: k > 1 by NAT_D: 52;

        per cases by A219;

          suppose

           A222: k <= 2;

          k >= (1 + 1) by A221, NAT_1: 13;

          then

           A223: k = 2 by A222, XXREAL_0: 1;

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

          then p1 in {(f /. (1 + 1))} by A218, A223, TOPREAL1:def 6;

          then p1 = (f /. (1 + 1)) by TARSKI:def 1;

          hence contradiction by A6, A17, A172, SPRECT_3: 5;

        end;

          suppose

           A224: (k + 1) >= ( len f);

          

           A225: (( LSeg (f,1)) /\ ( LSeg (f,(( len f) -' 1)))) = {(f . 1)} by JORDAN4: 42

          .= {(f /. 1)} by A15, PARTFUN1:def 6;

          ii <= (j -' l) by A212, A214, XREAL_1: 6;

          then (ii + l) <= j by A208, NAT_D: 54;

          then (ii + l) <= ( len f) by A209, XXREAL_0: 2;

          then

           A226: ((ii + l) -' 1) <= (( len f) -' 1) by NAT_D: 42;

          k >= (( len f) -' 1) by A224, NAT_D: 53;

          then k = (( len f) -' 1) by A226, XXREAL_0: 1;

          hence contradiction by A1, A172, A218, A225, TARSKI:def 1;

        end;

      end;

      ( LSeg ((f /. 1),(f /. 2))) c= ( L~ ( SpStSeq ( L~ f))) by A1, SPRECT_3: 31;

      then

       A227: (( L~ ( SpStSeq ( L~ f))) /\ ( LSeg (p1,z2))) = {p1} by A65, A82, A165, SPRECT_3: 48;

      

       A228: ( LSeg (p1,(f /. 2))) is horizontal by A80, A170, SPPOL_1: 15;

      

       A229: p1 in ( LSeg (p1,(f /. 2))) by RLTOPSP1: 68;

      then

       A230: p1 in ( L~ f) by A169;

      

       A231: <*p1*> is_in_the_area_of f by A169, A229, SPRECT_2: 21, SPRECT_3: 46;

      

       A232: ( L~ f) misses ( L~ Red9) by A51, A53, SPRECT_3: 25, XBOOLE_1: 63;

      reconsider Red9 as S-Sequence_in_R2 by A52;

      ( len Red9) in ( dom Red9) by FINSEQ_5: 6;

      then

       A233: z2 in ( L~ Red9) by A55, SPPOL_2: 44;

      set u1 = ( Last_Point (( L~ Red9),(Red9 /. 1),(Red9 /. ( len Red9)),( L~ ( SpStSeq ( L~ f))))), Red = ( L_Cut (Red9,u1)), u2 = ( First_Point (( L~ Red),(Red /. 1),(Red /. ( len Red)),( LSeg (z2,p1)))), u3 = ( First_Point (( L~ Red),(Red /. 1),(Red /. ( len Red)),( LSeg (z2,p2))));

      ( NW-corner ( L~ ( SpStSeq ( L~ f)))) = ( NW-corner ( L~ f)) by SPRECT_1: 62;

      then

       A234: u1 <> ( NW-corner ( L~ f)) by A47, A48, A54, A55, SPRECT_3: 38;

      

       A235: ( L~ Red9) is_an_arc_of (z1,z2) by A54, A55, TOPREAL1: 25;

      (( L~ Red9) /\ ( L~ ( SpStSeq ( L~ f)))) is closed by TOPS_1: 8;

      then

       A236: u1 in (( L~ Red9) /\ ( L~ ( SpStSeq ( L~ f)))) by A54, A55, A56, A235, JORDAN5C:def 2;

      then

       A237: u1 in ( L~ ( SpStSeq ( L~ f))) by XBOOLE_0:def 4;

      

       A238: u1 in ( L~ Red9) by A236, XBOOLE_0:def 4;

       A239:

      now

        assume u1 in ( L~ f);

        then u1 in (( L~ f) /\ ( L~ Red9)) by A238, XBOOLE_0:def 4;

        hence contradiction by A232, XBOOLE_0:def 7;

      end;

      ( len Red9) in ( dom Red9) by FINSEQ_5: 6;

      then u1 <> (Red9 . ( len Red9)) by A55, A65, A237, PARTFUN1:def 6;

      then

      reconsider Red as S-Sequence_in_R2 by A238, JORDAN3: 34;

      1 in ( dom Red) by FINSEQ_5: 6;

      

      then

       A240: (Red /. 1) = (Red . 1) by PARTFUN1:def 6

      .= u1 by A238, JORDAN3: 23;

      

       A241: (( L~ ( SpStSeq ( L~ f))) /\ ( L~ Red)) = {u1} by A55, A56, A65, Th5;

      ( len Red9) in ( dom Red9) by FINSEQ_5: 6;

      then z2 = (Red9 . ( len Red9)) by A55, PARTFUN1:def 6;

      then

       A242: z2 in ( L~ Red) by A65, A233, A237, A238, JORDAN5B: 22;

      Red is_in_the_area_of ( SpStSeq ( L~ f)) by A47, A48, A54, A55, SPRECT_3: 54;

      then

       A243: Red is_in_the_area_of f by SPRECT_3: 53;

      

       A244: ( L~ Red) c= ( L~ Red9) by A238, JORDAN3: 42;

      

       A245: ( L~ f) misses ( L~ Red) by A232, A238, JORDAN3: 42, XBOOLE_1: 63;

      z2 in ( LSeg (p1,z2)) by RLTOPSP1: 68;

      then

       A246: ( LSeg (p1,z2)) meets ( L~ Red) by A242, XBOOLE_0: 3;

      z2 in ( LSeg (p2,z2)) by RLTOPSP1: 68;

      then

       A247: ( LSeg (p2,z2)) meets ( L~ Red) by A242, XBOOLE_0: 3;

      

       A248: (( L~ Red) /\ ( LSeg (p1,z2))) is closed by TOPS_1: 8;

      

       A249: (( L~ Red) /\ ( LSeg (p2,z2))) is closed by TOPS_1: 8;

      ( L~ Red) is_an_arc_of ((Red /. 1),(Red /. ( len Red))) by TOPREAL1: 25;

      then

       A250: u3 in (( LSeg (p2,z2)) /\ ( L~ Red)) by A247, A249, JORDAN5C:def 1;

      then

       A251: u3 in ( L~ Red) by XBOOLE_0:def 4;

      

       A252: u3 in ( LSeg (p2,z2)) by A250, XBOOLE_0:def 4;

      

       A253: u3 <> p2 by A94, A98, A232, A244, A251, XBOOLE_0: 3;

      

       A254: p2 in ( LSeg (p2,z2)) by RLTOPSP1: 68;

      then

       A255: ( LSeg (p2,u3)) c= ( LSeg (p2,z2)) by A252, TOPREAL1: 6;

      then

       A256: ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) misses ( LSeg (u3,p2)) by A71, A88, A135, SPRECT_3: 9, XBOOLE_1: 63;

      

       A257: for i, j st 1 <= i & i < j & j < ( len f) holds ( L~ ( mid (f,i,j))) misses ( LSeg (u3,p2))

      proof

        let i, j;

        assume that

         A258: 1 <= i and

         A259: i < j and

         A260: j < ( len f);

        ( L~ ( mid (f,i,j))) misses ( LSeg (z2,p2)) by A139, A258, A259, A260;

        hence thesis by A252, A254, TOPREAL1: 6, XBOOLE_1: 63;

      end;

       A261:

      now

        

         A262: 1 in ( dom Red) by FINSEQ_5: 6;

        assume u3 = (Red . 1);

        then u3 in ( L~ ( SpStSeq ( L~ f))) by A237, A240, A262, PARTFUN1:def 6;

        then u3 in (( LSeg (p2,z2)) /\ ( L~ ( SpStSeq ( L~ f)))) by A252, XBOOLE_0:def 4;

        hence contradiction by A162, A253, TARSKI:def 1;

      end;

      ( L~ Red) is_an_arc_of ((Red /. 1),(Red /. ( len Red))) by TOPREAL1: 25;

      then

       A263: u2 in (( LSeg (p1,z2)) /\ ( L~ Red)) by A246, A248, JORDAN5C:def 1;

      then

       A264: u2 in ( L~ Red) by XBOOLE_0:def 4;

      

       A265: u2 in ( LSeg (p1,z2)) by A263, XBOOLE_0:def 4;

      

       A266: u2 <> p1 by A169, A229, A232, A244, A264, XBOOLE_0: 3;

      

       A267: p1 in ( LSeg (p1,z2)) by RLTOPSP1: 68;

      then

       A268: ( LSeg (p1,u2)) c= ( LSeg (p1,z2)) by A265, TOPREAL1: 6;

      

       A269: ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) misses ( LSeg (u2,p1)) by A199, A265, A267, TOPREAL1: 6, XBOOLE_1: 63;

      

       A270: for i, j st 1 < i & i < j & j <= ( len f) holds ( L~ ( mid (f,i,j))) misses ( LSeg (u2,p1))

      proof

        let i, j;

        assume that

         A271: 1 < i and

         A272: i < j and

         A273: j <= ( len f);

        ( L~ ( mid (f,i,j))) misses ( LSeg (z2,p1)) by A203, A271, A272, A273;

        hence thesis by A265, A267, TOPREAL1: 6, XBOOLE_1: 63;

      end;

       A274:

      now

        

         A275: 1 in ( dom Red) by FINSEQ_5: 6;

        assume u2 = (Red . 1);

        then u2 in ( L~ ( SpStSeq ( L~ f))) by A237, A240, A275, PARTFUN1:def 6;

        then u2 in {p1} by A227, A265, XBOOLE_0:def 4;

        hence contradiction by A266, TARSKI:def 1;

      end;

      reconsider Red2 = ( R_Cut (Red,u3)) as S-Sequence_in_R2 by A251, A261, JORDAN3: 35;

      

       A276: (Red2 /. 1) = u1 by A240, A251, SPRECT_3: 22;

      

       A277: ( len Red2) in ( dom Red2) by FINSEQ_5: 6;

      

       A278: (( Rev Red2) /. 1) = (Red2 /. ( len Red2)) by FINSEQ_5: 65

      .= (Red2 . ( len Red2)) by A277, PARTFUN1:def 6

      .= u3 by A251, JORDAN3: 24;

      then

       A279: ((( Rev Red2) /. 1) `2 ) = (p2 `2 ) by A88, A252, SPPOL_1: 40;

      

       A280: (( Rev Red2) /. 1) <> p2 by A94, A98, A232, A244, A251, A278, XBOOLE_0: 3;

      

       A281: ( L~ ( Rev Red2)) = ( L~ Red2) by SPPOL_2: 22;

      

       A282: u3 in ( L~ Red2) by A251, A261, JORDAN5B: 20;

      u3 in ( LSeg (p2,u3)) by RLTOPSP1: 68;

      then

       A283: u3 in (( L~ Red2) /\ ( LSeg (p2,u3))) by A282, XBOOLE_0:def 4;

      now

        assume u1 in ( LSeg (p2,z2));

        then u1 in (( L~ ( SpStSeq ( L~ f))) /\ ( LSeg (p2,z2))) by A237, XBOOLE_0:def 4;

        hence contradiction by A99, A162, A239, TARSKI:def 1;

      end;

      then (( LSeg (p2,z2)) /\ ( L~ Red2)) = {u3} by A240, A247, Th1;

      then (( LSeg (p2,u3)) /\ ( L~ Red2)) c= {u3} by A252, A254, TOPREAL1: 6, XBOOLE_1: 26;

      then (( LSeg (p2,u3)) /\ ( L~ Red2)) = {u3} by A283, ZFMISC_1: 33;

      then

      reconsider RB2 = ( <*p2*> ^ ( Rev Red2)) as S-Sequence_in_R2 by A278, A279, A280, A281, SPRECT_3: 16;

      ( LSeg (p2,(f /. (( len f) -' 1)))) misses ( L~ Red) by A92, A93, A245, XBOOLE_1: 1, XBOOLE_1: 63;

      then ( LSeg (p2,(f /. (( len f) -' 1)))) misses ( L~ Red2) by A251, JORDAN3: 41, XBOOLE_1: 63;

      then

       A284: (( LSeg (p2,(f /. (( len f) -' 1)))) /\ ( L~ Red2)) = {} by XBOOLE_0:def 7;

      1 in ( dom Red2) by FINSEQ_5: 6;

      then u1 in ( L~ Red2) by A276, SPPOL_2: 44;

      then

       A285: u1 in (( L~ ( SpStSeq ( L~ f))) /\ ( L~ Red2)) by A237, XBOOLE_0:def 4;

      (( L~ ( SpStSeq ( L~ f))) /\ ( L~ Red2)) c= {u1} by A241, A251, JORDAN3: 41, XBOOLE_1: 26;

      then

       A286: (( L~ ( SpStSeq ( L~ f))) /\ ( L~ Red2)) = {u1} by A285, ZFMISC_1: 33;

      reconsider Red1 = ( R_Cut (Red,u2)) as S-Sequence_in_R2 by A264, A274, JORDAN3: 35;

      ( len Red1) in ( dom Red1) by FINSEQ_5: 6;

      

      then

       A287: (Red1 /. ( len Red1)) = (Red1 . ( len Red1)) by PARTFUN1:def 6

      .= u2 by A264, JORDAN3: 24;

      

       A288: (Red1 /. 1) = u1 by A240, A264, SPRECT_3: 22;

      

       A289: ((Red1 /. ( len Red1)) `1 ) = (p1 `1 ) by A163, A265, A287, SPPOL_1: 41;

      

       A290: (Red1 /. ( len Red1)) <> p1 by A169, A229, A232, A244, A264, A287, XBOOLE_0: 3;

      

       A291: u2 in ( L~ Red1) by A264, A274, JORDAN5B: 20;

      u2 in ( LSeg (p1,u2)) by RLTOPSP1: 68;

      then

       A292: u2 in (( L~ Red1) /\ ( LSeg (p1,u2))) by A291, XBOOLE_0:def 4;

      now

        assume u1 in ( LSeg (p1,z2));

        then u1 in (( L~ ( SpStSeq ( L~ f))) /\ ( LSeg (p1,z2))) by A237, XBOOLE_0:def 4;

        hence contradiction by A227, A230, A239, TARSKI:def 1;

      end;

      then (( LSeg (p1,z2)) /\ ( L~ Red1)) = {u2} by A240, A246, Th1;

      then (( LSeg (p1,u2)) /\ ( L~ Red1)) c= {u2} by A265, A267, TOPREAL1: 6, XBOOLE_1: 26;

      then (( LSeg (p1,u2)) /\ ( L~ Red1)) = {u2} by A292, ZFMISC_1: 33;

      then

      reconsider RB1 = (Red1 ^ <*p1*>) as S-Sequence_in_R2 by A287, A289, A290, SPRECT_2: 61;

      ( LSeg (p1,(f /. 2))) misses ( L~ Red) by A166, A168, A245, XBOOLE_1: 1, XBOOLE_1: 63;

      then ( LSeg (p1,(f /. 2))) misses ( L~ Red1) by A264, JORDAN3: 41, XBOOLE_1: 63;

      then

       A293: (( LSeg (p1,(f /. 2))) /\ ( L~ Red1)) = {} by XBOOLE_0:def 7;

      1 in ( dom Red1) by FINSEQ_5: 6;

      then

       A294: u1 in ( L~ Red1) by A288, SPPOL_2: 44;

      then

       A295: u1 in (( L~ ( SpStSeq ( L~ f))) /\ ( L~ Red1)) by A237, XBOOLE_0:def 4;

      (( L~ ( SpStSeq ( L~ f))) /\ ( L~ Red1)) c= {u1} by A241, A264, JORDAN3: 41, XBOOLE_1: 26;

      then

       A296: (( L~ ( SpStSeq ( L~ f))) /\ ( L~ Red1)) = {u1} by A295, ZFMISC_1: 33;

      ( len ( Rev Red2)) = ( len Red2) by FINSEQ_5:def 3;

      

      then

       A297: (RB2 /. ( len RB2)) = (( Rev Red2) /. ( len Red2)) by SPRECT_3: 1

      .= u1 by A276, FINSEQ_5: 65;

      

       A298: (RB2 /. 1) = p2 by FINSEQ_5: 15;

      ( L~ ( Rev Red2)) = ( L~ Red2) by SPPOL_2: 22;

      then

       A299: ( L~ RB2) = (( L~ Red2) \/ ( LSeg (p2,u3))) by A278, SPPOL_2: 20;

      

      then

       A300: (( LSeg (p2,(f /. (( len f) -' 1)))) /\ ( L~ RB2)) = ( {} \/ (( LSeg (p2,(f /. (( len f) -' 1)))) /\ ( LSeg (u3,p2)))) by A284, XBOOLE_1: 23

      .= {p2} by A88, A97, A255, SPRECT_1: 9, SPRECT_3: 10;

       <*u3*> is_in_the_area_of f by A243, A251, SPRECT_3: 46;

      then Red2 is_in_the_area_of f by A243, A251, SPRECT_3: 52;

      then ( Rev Red2) is_in_the_area_of f by SPRECT_3: 51;

      then

       A301: RB2 is_in_the_area_of f by A160, SPRECT_2: 24;

      1 in ( dom Red1) by FINSEQ_5: 6;

      then

       A302: (RB1 /. 1) = u1 by A288, FINSEQ_4: 68;

      ( len <*p1*>) = 1 by FINSEQ_1: 39;

      then ( len RB1) = (( len Red1) + 1) by FINSEQ_1: 22;

      then

       A303: (RB1 /. ( len RB1)) = p1 by FINSEQ_4: 67;

      

       A304: ( L~ RB1) = (( L~ Red1) \/ ( LSeg (u2,p1))) by A287, SPPOL_2: 19;

      

      then

       A305: (( LSeg (p1,(f /. 2))) /\ ( L~ RB1)) = ( {} \/ (( LSeg (p1,(f /. 2))) /\ ( LSeg (u2,p1)))) by A293, XBOOLE_1: 23

      .= {p1} by A163, A228, A268, SPRECT_1: 10, SPRECT_3: 10;

       <*u2*> is_in_the_area_of f by A243, A264, SPRECT_3: 46;

      then Red1 is_in_the_area_of f by A243, A264, SPRECT_3: 52;

      then

       A306: RB1 is_in_the_area_of f by A231, SPRECT_2: 24;

      

       A307: ( L~ Red9) is_an_arc_of (z1,z2) by A50, A53, TOPREAL4: 2;

      (( L~ Red9) /\ ( L~ ( SpStSeq ( L~ f)))) is closed by TOPS_1: 8;

      then u1 in (( L~ Red9) /\ ( L~ ( SpStSeq ( L~ f)))) by A54, A55, A56, A307, JORDAN5C:def 2;

      then u1 in ( L~ ( SpStSeq ( L~ f))) by XBOOLE_0:def 4;

      then u1 in ((( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) \/ ( LSeg (( NE-corner ( L~ f)),( SE-corner ( L~ f))))) \/ (( LSeg (( SE-corner ( L~ f)),( SW-corner ( L~ f)))) \/ ( LSeg (( SW-corner ( L~ f)),( NW-corner ( L~ f)))))) by SPRECT_1: 41;

      then

       A308: u1 in (( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) \/ ( LSeg (( NE-corner ( L~ f)),( SE-corner ( L~ f))))) or u1 in (( LSeg (( SE-corner ( L~ f)),( SW-corner ( L~ f)))) \/ ( LSeg (( SW-corner ( L~ f)),( NW-corner ( L~ f))))) by XBOOLE_0:def 3;

      

       A309: ( N-most ( L~ f)) c= ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) by XBOOLE_1: 17;

      

       A310: A in ( N-most ( L~ f)) by PSCOMP_1: 42;

      then ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) = (( LSeg (( NW-corner ( L~ f)),A)) \/ ( LSeg (A,( NE-corner ( L~ f))))) by A309, TOPREAL1: 5;

      then

       A311: u1 in ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) implies u1 in ( LSeg (( NW-corner ( L~ f)),A)) or u1 in ( LSeg (A,( NE-corner ( L~ f)))) by XBOOLE_0:def 3;

      per cases by A308, A311, XBOOLE_0:def 3;

        suppose

         A312: u1 in ( LSeg (( NW-corner ( L~ f)),A));

        

         A313: ( NW-corner ( L~ f)) in ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) by RLTOPSP1: 68;

        then ( LSeg (( NW-corner ( L~ f)),A)) c= ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) by A309, A310, TOPREAL1: 6;

        then ( LSeg (( NW-corner ( L~ f)),u1)) c= ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) by A312, A313, TOPREAL1: 6;

        then ( LSeg (( NW-corner ( L~ f)),u1)) c= ( L~ ( SpStSeq ( L~ f))) by A66, XBOOLE_1: 1;

        then

         A314: (( LSeg (( NW-corner ( L~ f)),u1)) /\ ( L~ Red1)) c= {u1} by A296, XBOOLE_1: 26;

        

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

        

         A316: ( NW-corner ( L~ f)) in ( LSeg (( NW-corner ( L~ f)),A)) by RLTOPSP1: 68;

        then ( LSeg (( NW-corner ( L~ f)),u1)) misses ( LSeg (u2,p1)) by A269, A312, TOPREAL1: 6, XBOOLE_1: 63;

        then

         A317: (( LSeg (( NW-corner ( L~ f)),u1)) /\ ( LSeg (u2,p1))) = {} by XBOOLE_0:def 7;

        u1 in ( LSeg (( NW-corner ( L~ f)),u1)) by RLTOPSP1: 68;

        then u1 in (( LSeg (( NW-corner ( L~ f)),u1)) /\ ( L~ Red1)) by A294, XBOOLE_0:def 4;

        then {u1} c= (( LSeg (( NW-corner ( L~ f)),u1)) /\ ( L~ Red1)) by ZFMISC_1: 31;

        then (( LSeg (( NW-corner ( L~ f)),u1)) /\ ( L~ Red1)) = {u1} by A314, XBOOLE_0:def 10;

        

        then

         A318: (( LSeg (( NW-corner ( L~ f)),u1)) /\ ( L~ RB1)) = ( {u1} \/ {} ) by A304, A317, XBOOLE_1: 23

        .= {u1};

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

        then (u1 `2 ) = (( NW-corner ( L~ f)) `2 ) by A312, A315, GOBOARD7: 6;

        then

        reconsider M3 = ( <*( NW-corner ( L~ f))*> ^ RB1) as S-Sequence_in_R2 by A234, A302, A318, SPRECT_3: 16;

        

         A319: ( L~ M3) = (( LSeg (( NW-corner ( L~ f)),(RB1 /. 1))) \/ ( L~ RB1)) by SPPOL_2: 20;

        set i1 = (( S-min ( L~ f)) .. f), i2 = (( E-min ( L~ f)) .. f);

        (( N-max ( L~ f)) .. f) > 1 by A1, SPRECT_2: 69;

        then (( N-max ( L~ f)) .. f) >= (1 + 1) by NAT_1: 13;

        then 2 <= (( E-max ( L~ f)) .. f) by A1, SPRECT_2: 70, XXREAL_0: 2;

        then

         A320: 2 < i2 by A1, SPRECT_2: 71, XXREAL_0: 2;

        ( LSeg (p1,(f /. 2))) misses ( LSeg (( NW-corner ( L~ f)),u1)) by A196, A312, A316, TOPREAL1: 6, XBOOLE_1: 63;

        then (( LSeg (p1,(f /. 2))) /\ ( LSeg (( NW-corner ( L~ f)),u1))) = {} by XBOOLE_0:def 7;

        

        then

         A321: (( LSeg (p1,(f /. 2))) /\ ( L~ M3)) = ( {} \/ (( LSeg (p1,(f /. 2))) /\ ( L~ RB1))) by A302, A319, XBOOLE_1: 23

        .= {p1} by A305;

        

         A322: ( L~ M3) = (( LSeg (( NW-corner ( L~ f)),(RB1 /. 1))) \/ ( L~ RB1)) by SPPOL_2: 20;

        (( W-min ( L~ f)) .. f) < ( len f) by A1, SPRECT_2: 76;

        then

         A323: i1 < ( len f) by A1, SPRECT_2: 74, XXREAL_0: 2;

        

         A324: ( E-min ( L~ f)) in ( rng f) by SPRECT_2: 45;

        then

         A325: i2 in ( dom f) by FINSEQ_4: 20;

        then

         A326: i2 <= ( len f) by FINSEQ_3: 25;

        then

        reconsider M4 = ( mid (f,2,i2)) as S-Sequence_in_R2 by A320, JORDAN4: 40;

        ( L~ M4) misses ( L~ Red) by A57, A245, A325, SPRECT_3: 18, XBOOLE_1: 63;

        then

         A327: ( L~ M4) misses ( L~ Red1) by A264, JORDAN3: 41, XBOOLE_1: 63;

        (( S-max ( L~ f)) .. f) < i1 by A1, SPRECT_2: 73;

        then

         A328: i2 < i1 by A1, SPRECT_2: 72, XXREAL_0: 2;

        then

         A329: 2 < i1 by A320, XXREAL_0: 2;

        then 1 < i1 by XXREAL_0: 2;

        then

        reconsider M1 = ( mid (f,i1,( len f))) as S-Sequence_in_R2 by A323, JORDAN4: 40;

        

         A330: ( L~ M1) misses ( L~ M4) by A328, A323, A320, SPRECT_2: 47;

        

         A331: ( L~ M1) misses ( LSeg (p1,(f /. 2))) by A173, A323, A329;

        

         A332: ( len M1) >= 2 by TOPREAL1:def 8;

        

         A333: (M4 /. 1) = (f /. 2) by A57, A325, SPRECT_2: 8;

        ( L~ M4) misses ( LSeg (u2,p1)) by A270, A320, A326;

        then

         A334: ( L~ RB1) misses ( L~ M4) by A304, A327, XBOOLE_1: 70;

        

         A335: ( LSeg (( NW-corner ( L~ f)),u1)) c= ( LSeg (( NW-corner ( L~ f)),A)) by A312, A316, TOPREAL1: 6;

         A336:

        now

          

           A337: (( LSeg (( NW-corner ( L~ f)),A)) /\ ( L~ f)) = {A} by PSCOMP_1: 43;

          assume ( L~ f) meets ( LSeg (( NW-corner ( L~ f)),u1));

          then

          consider u be object such that

           A338: u in ( L~ f) and

           A339: u in ( LSeg (( NW-corner ( L~ f)),u1)) by XBOOLE_0: 3;

          reconsider u as Point of ( TOP-REAL 2) by A338;

          u in (( LSeg (( NW-corner ( L~ f)),A)) /\ ( L~ f)) by A335, A338, A339, XBOOLE_0:def 4;

          then u = A by A337, TARSKI:def 1;

          hence contradiction by A239, A312, A338, A339, SPRECT_3: 6;

        end;

        then ( L~ M4) misses ( LSeg (( NW-corner ( L~ f)),u1)) by A57, A325, SPRECT_3: 18, XBOOLE_1: 63;

        then

         A340: ( L~ M3) misses ( L~ M4) by A302, A319, A334, XBOOLE_1: 70;

        

         A341: ( S-min ( L~ f)) in ( rng f) by SPRECT_2: 41;

        then

         A342: i1 in ( dom f) by FINSEQ_4: 20;

        then

         A343: M1 is_in_the_area_of f by A58, SPRECT_2: 23;

        

         A344: ((M1 /. ( len M1)) `2 ) = ((f /. ( len f)) `2 ) by A58, A342, SPRECT_2: 9

        .= ((f /. 1) `2 ) by FINSEQ_6:def 1

        .= ( N-bound ( L~ f)) by A1, EUCLID: 52;

        ((M1 /. 1) `2 ) = ((f /. i1) `2 ) by A58, A342, SPRECT_2: 8

        .= (( S-min ( L~ f)) `2 ) by A341, FINSEQ_5: 38

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

        then

         A345: M1 is_a_v.c._for f by A343, A344, SPRECT_2:def 3;

        

         A346: ( <*( NW-corner ( L~ f))*> ^ RB1) is_in_the_area_of f by A63, A306, SPRECT_2: 24;

        1 < i1 by A329, XXREAL_0: 2;

        then

         A347: ( L~ M1) misses ( LSeg (u2,p1)) by A270, A323;

        

         A348: (M3 /. ( len M3)) = p1 by A303, SPRECT_3: 1;

        (( LSeg (p1,(f /. 2))) /\ ( L~ M4)) = {(f /. 2)} by A191, A320, A326;

        then

        reconsider M2 = (M3 ^ M4) as S-Sequence_in_R2 by A80, A170, A348, A333, A340, A321, SPRECT_3: 21;

        M2 = ( <*( NW-corner ( L~ f))*> ^ (RB1 ^ ( mid (f,2,i2)))) by FINSEQ_1: 32;

        

        then

         A349: ((M2 /. 1) `1 ) = (( NW-corner ( L~ f)) `1 ) by FINSEQ_5: 15

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

        ( mid (f,2,i2)) is_in_the_area_of f by A57, A325, SPRECT_2: 23;

        then

         A350: M2 is_in_the_area_of f by A346, SPRECT_2: 24;

        ((M2 /. ( len M2)) `1 ) = ((( mid (f,2,i2)) /. ( len ( mid (f,2,i2)))) `1 ) by SPRECT_3: 1

        .= ((f /. i2) `1 ) by A57, A325, SPRECT_2: 9

        .= (( E-min ( L~ f)) `1 ) by A324, FINSEQ_5: 38

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

        then

         A351: M2 is_a_h.c._for f by A350, A349, SPRECT_2:def 2;

        

         A352: ( L~ M2) = ((( L~ M3) \/ ( LSeg ((M3 /. ( len M3)),(M4 /. 1)))) \/ ( L~ M4)) by SPPOL_2: 23;

        ( len M2) >= 2 by TOPREAL1:def 8;

        then ( L~ M1) meets ( L~ M2) by A332, A345, A351, SPRECT_2: 29;

        then ( L~ M1) meets (( L~ M3) \/ ( LSeg ((M3 /. ( len M3)),(M4 /. 1)))) by A352, A330, XBOOLE_1: 70;

        then

         A353: ( L~ M1) meets ( L~ M3) by A348, A333, A331, XBOOLE_1: 70;

        ( L~ M1) misses ( LSeg (( NW-corner ( L~ f)),u1)) by A58, A342, A336, SPRECT_3: 18, XBOOLE_1: 63;

        then ( L~ M1) meets ( L~ RB1) by A302, A353, A322, XBOOLE_1: 70;

        then ( L~ M1) meets ( L~ Red1) by A304, A347, XBOOLE_1: 70;

        then ( L~ M1) meets ( L~ Red) by A264, JORDAN3: 41, XBOOLE_1: 63;

        hence contradiction by A58, A245, A342, SPRECT_3: 18, XBOOLE_1: 63;

      end;

        suppose that

         A354: u1 in ( LSeg (A,( NE-corner ( L~ f)))) and

         A355: ( N-min ( L~ f)) = ( NW-corner ( L~ f));

        set i1 = (( S-max ( L~ f)) .. f), i2 = (( E-max ( L~ f)) .. f);

        (( N-max ( L~ f)) .. f) > 1 by A1, SPRECT_2: 69;

        then

         A356: 1 < i2 by A1, SPRECT_2: 70, XXREAL_0: 2;

        (( S-min ( L~ f)) .. f) <= (( W-min ( L~ f)) .. f) by A1, SPRECT_2: 74;

        then (( S-max ( L~ f)) .. f) < (( W-min ( L~ f)) .. f) by A1, SPRECT_2: 73, XXREAL_0: 2;

        then ((( S-max ( L~ f)) .. f) + 1) <= (( W-min ( L~ f)) .. f) by NAT_1: 13;

        then ((( S-max ( L~ f)) .. f) + 1) < ( len f) by A1, SPRECT_2: 76, XXREAL_0: 2;

        then

         A357: i1 < (( len f) -' 1) by A61, XREAL_1: 6;

        (( E-max ( L~ f)) .. f) < (( E-min ( L~ f)) .. f) by A1, SPRECT_2: 71;

        then

         A358: i2 < i1 by A1, SPRECT_2: 72, XXREAL_0: 2;

        then

         A359: 1 < i1 by A356, XXREAL_0: 2;

        then

        reconsider M4 = ( mid (f,i1,(( len f) -' 1))) as S-Sequence_in_R2 by A61, A357, JORDAN4: 39;

        

         A360: ( L~ M4) misses ( LSeg (u3,p2)) by A62, A257, A357, A359;

        i1 < ( len f) by A357, NAT_D: 44;

        then

         A361: i2 < ( len f) by A358, XXREAL_0: 2;

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

        then

        reconsider M2 = ( mid (f,1,i2)) as S-Sequence_in_R2 by A356, JORDAN4: 39;

        

         A362: ( L~ M2) misses ( L~ M4) by A62, A358, A357, A356, SPRECT_2: 47;

        i2 < (( len f) -' 1) by A358, A357, XXREAL_0: 2;

        then

         A363: ( L~ M2) misses ( LSeg (p2,(f /. (( len f) -' 1)))) by A105, A356;

        

         A364: ( len M2) >= 2 by TOPREAL1:def 8;

        

         A365: ( L~ M2) misses ( LSeg (u3,p2)) by A257, A356, A361;

        

         A366: ( E-max ( L~ f)) in ( rng f) by SPRECT_2: 46;

        then

         A367: i2 in ( dom f) by FINSEQ_4: 20;

        

        then

         A368: ((M2 /. ( len M2)) `1 ) = ((f /. i2) `1 ) by A15, SPRECT_2: 9

        .= (( E-max ( L~ f)) `1 ) by A366, FINSEQ_5: 38

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

        

         A369: ( S-max ( L~ f)) in ( rng f) by SPRECT_2: 42;

        then

         A370: i1 in ( dom f) by FINSEQ_4: 20;

        then ( L~ M4) misses ( L~ Red) by A60, A245, SPRECT_3: 18, XBOOLE_1: 63;

        then ( L~ M4) misses ( L~ Red2) by A251, JORDAN3: 41, XBOOLE_1: 63;

        then

         A371: ( L~ RB2) misses ( L~ M4) by A299, A360, XBOOLE_1: 70;

        

         A372: M2 is_in_the_area_of f by A15, A367, SPRECT_2: 23;

        ((M2 /. 1) `1 ) = ((f /. 1) `1 ) by A15, A367, SPRECT_2: 8

        .= ( W-bound ( L~ f)) by A1, A355, EUCLID: 52;

        then

         A373: M2 is_a_h.c._for f by A372, A368, SPRECT_2:def 2;

        

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

        

         A375: (( NE-corner ( L~ f)) `2 ) = ( N-bound ( L~ f)) by EUCLID: 52;

        

         A376: (M4 /. ( len M4)) = (f /. (( len f) -' 1)) by A60, A370, SPRECT_2: 9;

        then (( LSeg ((M4 /. ( len M4)),p2)) /\ ( L~ M4)) = {(M4 /. ( len M4))} by A126, A357, A359;

        then

        reconsider M1 = (M4 ^ RB2) as S-Sequence_in_R2 by A78, A83, A96, A298, A300, A376, A371, SPRECT_3: 21;

        ( mid (f,i1,(( len f) -' 1))) is_in_the_area_of f by A60, A370, SPRECT_2: 23;

        then

         A377: M1 is_in_the_area_of f by A301, SPRECT_2: 24;

        

         A378: ((M1 /. ( len M1)) `2 ) = ((RB2 /. ( len RB2)) `2 ) by SPRECT_3: 1

        .= ( N-bound ( L~ f)) by A297, A354, A375, A374, GOBOARD7: 6;

        ( mid (f,i1,(( len f) -' 1))) is non empty by A60, A370, SPRECT_2: 7;

        then 1 in ( dom ( mid (f,i1,(( len f) -' 1)))) by FINSEQ_5: 6;

        

        then ((M1 /. 1) `2 ) = ((( mid (f,i1,(( len f) -' 1))) /. 1) `2 ) by FINSEQ_4: 68

        .= ((f /. i1) `2 ) by A60, A370, SPRECT_2: 8

        .= (( S-max ( L~ f)) `2 ) by A369, FINSEQ_5: 38

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

        then

         A379: M1 is_a_v.c._for f by A377, A378, SPRECT_2:def 3;

        

         A380: ( L~ M1) = ((( L~ M4) \/ ( LSeg ((M4 /. ( len M4)),p2))) \/ ( L~ RB2)) by A298, SPPOL_2: 23

        .= (( L~ M4) \/ (( LSeg ((M4 /. ( len M4)),p2)) \/ ( L~ RB2))) by XBOOLE_1: 4;

        ( len M1) >= 2 by TOPREAL1:def 8;

        then ( L~ M1) meets ( L~ M2) by A364, A379, A373, SPRECT_2: 29;

        then ( L~ M2) meets (( L~ RB2) \/ ( LSeg (p2,(M4 /. ( len M4))))) by A380, A362, XBOOLE_1: 70;

        then ( L~ M2) meets ( L~ RB2) by A376, A363, XBOOLE_1: 70;

        then ( L~ M2) meets ( L~ Red2) by A299, A365, XBOOLE_1: 70;

        then ( L~ M2) meets ( L~ Red) by A251, JORDAN3: 41, XBOOLE_1: 63;

        hence contradiction by A15, A245, A367, SPRECT_3: 18, XBOOLE_1: 63;

      end;

        suppose that

         A381: u1 in ( LSeg (A,( NE-corner ( L~ f)))) and

         A382: ( N-min ( L~ f)) <> ( NW-corner ( L~ f));

        set i1 = (( S-min ( L~ f)) .. f), i2 = (( E-max ( L~ f)) .. f);

        

         A383: (( S-min ( L~ f)) .. f) <= (( W-min ( L~ f)) .. f) by A1, SPRECT_2: 74;

        ( W-max ( L~ f)) <> ( N-min ( L~ f)) by A382, PSCOMP_1: 61;

        then (( S-min ( L~ f)) .. f) < (( W-max ( L~ f)) .. f) by A1, A383, SPRECT_2: 75, XXREAL_0: 2;

        then ((( S-min ( L~ f)) .. f) + 1) <= (( W-max ( L~ f)) .. f) by NAT_1: 13;

        then ((( S-min ( L~ f)) .. f) + 1) < ( len f) by A1, SPRECT_2: 77, XXREAL_0: 2;

        then

         A384: i1 < (( len f) -' 1) by A61, XREAL_1: 6;

        

         A385: ( N-min ( L~ f)) in ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) by RLTOPSP1: 68;

        

         A386: (( N-min ( L~ f)) `2 ) = (( NW-corner ( L~ f)) `2 ) by PSCOMP_1: 37;

        (( N-max ( L~ f)) .. f) > 1 by A1, SPRECT_2: 69;

        then

         A387: 1 < i2 by A1, SPRECT_2: 70, XXREAL_0: 2;

        (( E-max ( L~ f)) .. f) < (( E-min ( L~ f)) .. f) by A1, SPRECT_2: 71;

        then (( E-max ( L~ f)) .. f) < (( S-max ( L~ f)) .. f) by A1, SPRECT_2: 72, XXREAL_0: 2;

        then

         A388: i2 < i1 by A1, SPRECT_2: 73, XXREAL_0: 2;

        then

         A389: 1 < i1 by A387, XXREAL_0: 2;

        then

        reconsider M4 = ( mid (f,i1,(( len f) -' 1))) as S-Sequence_in_R2 by A61, A384, JORDAN4: 39;

        

         A390: ( L~ M4) misses ( LSeg (u3,p2)) by A62, A257, A384, A389;

        i1 < ( len f) by A384, NAT_D: 44;

        then

         A391: i2 < ( len f) by A388, XXREAL_0: 2;

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

        then

        reconsider M3 = ( mid (f,1,i2)) as S-Sequence_in_R2 by A387, JORDAN4: 39;

        

         A392: ( L~ M3) misses ( L~ M4) by A62, A388, A384, A387, SPRECT_2: 47;

        i2 < (( len f) -' 1) by A388, A384, XXREAL_0: 2;

        then

         A393: ( L~ M3) misses ( LSeg (p2,(f /. (( len f) -' 1)))) by A105, A387;

        

         A394: ( L~ M3) misses ( LSeg (u3,p2)) by A257, A387, A391;

        

         A395: ( E-max ( L~ f)) in ( rng f) by SPRECT_2: 46;

        then

         A396: i2 in ( dom f) by FINSEQ_4: 20;

        then

         A397: (M3 /. 1) = ( N-min ( L~ f)) by A1, A15, SPRECT_2: 8;

        

         A398: ( S-min ( L~ f)) in ( rng f) by SPRECT_2: 41;

        then

         A399: i1 in ( dom f) by FINSEQ_4: 20;

        then ( L~ M4) misses ( L~ Red) by A60, A245, SPRECT_3: 18, XBOOLE_1: 63;

        then ( L~ M4) misses ( L~ Red2) by A251, JORDAN3: 41, XBOOLE_1: 63;

        then

         A400: ( L~ RB2) misses ( L~ M4) by A299, A390, XBOOLE_1: 70;

        

         A401: (M4 /. ( len M4)) = (f /. (( len f) -' 1)) by A60, A399, SPRECT_2: 9;

        then (( LSeg ((M4 /. ( len M4)),p2)) /\ ( L~ M4)) = {(M4 /. ( len M4))} by A126, A384, A389;

        then

        reconsider M1 = (M4 ^ RB2) as S-Sequence_in_R2 by A78, A83, A96, A298, A300, A401, A400, SPRECT_3: 21;

        

         A402: ( L~ M1) = ((( L~ M4) \/ ( LSeg ((M4 /. ( len M4)),p2))) \/ ( L~ RB2)) by A298, SPPOL_2: 23

        .= (( L~ M4) \/ (( LSeg ((M4 /. ( len M4)),p2)) \/ ( L~ RB2))) by XBOOLE_1: 4;

        1 in ( dom M3) by FINSEQ_5: 6;

        then ( N-min ( L~ f)) in ( L~ M3) by A397, SPPOL_2: 44;

        then ( N-min ( L~ f)) in (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ M3)) by A385, XBOOLE_0:def 4;

        then

         A403: {( N-min ( L~ f))} c= (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ M3)) by ZFMISC_1: 31;

        

         A404: (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ f)) = {( N-min ( L~ f))} by PSCOMP_1: 43;

        then (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ M3)) c= {( N-min ( L~ f))} by A15, A396, SPRECT_3: 18, XBOOLE_1: 26;

        then (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ M3)) = {( N-min ( L~ f))} by A403, XBOOLE_0:def 10;

        then

        reconsider M2 = ( <*( NW-corner ( L~ f))*> ^ M3) as S-Sequence_in_R2 by A382, A386, A397, SPRECT_3: 16;

        

         A405: ((M2 /. 1) `1 ) = (( NW-corner ( L~ f)) `1 ) by FINSEQ_5: 15

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

         A406:

        now

          assume ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) meets ( L~ M4);

          then

           A407: (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ M4)) <> {} by XBOOLE_0:def 7;

          (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ M4)) c= {( N-min ( L~ f))} by A60, A399, A404, SPRECT_3: 18, XBOOLE_1: 26;

          then (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ M4)) = {( N-min ( L~ f))} by A407, ZFMISC_1: 33;

          then ( N-min ( L~ f)) in (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ M4)) by TARSKI:def 1;

          then ( N-min ( L~ f)) in ( L~ M4) by XBOOLE_0:def 4;

          hence contradiction by A1, A62, A384, A389, SPRECT_3: 30;

        end;

        

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

        

         A409: (( NE-corner ( L~ f)) `2 ) = ( N-bound ( L~ f)) by EUCLID: 52;

        ( mid (f,1,i2)) is_in_the_area_of f by A15, A396, SPRECT_2: 23;

        then

         A410: M2 is_in_the_area_of f by A63, SPRECT_2: 24;

        ((M2 /. ( len M2)) `1 ) = ((( mid (f,1,i2)) /. ( len ( mid (f,1,i2)))) `1 ) by SPRECT_3: 1

        .= ((f /. i2) `1 ) by A15, A396, SPRECT_2: 9

        .= (( E-max ( L~ f)) `1 ) by A395, FINSEQ_5: 38

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

        then

         A411: M2 is_a_h.c._for f by A410, A405, SPRECT_2:def 2;

        

         A412: ( L~ M2) = (( LSeg (( NW-corner ( L~ f)),(M3 /. 1))) \/ ( L~ M3)) by SPPOL_2: 20;

        ( mid (f,i1,(( len f) -' 1))) is_in_the_area_of f by A60, A399, SPRECT_2: 23;

        then

         A413: M1 is_in_the_area_of f by A301, SPRECT_2: 24;

        

         A414: ((M1 /. ( len M1)) `2 ) = (u1 `2 ) by A297, SPRECT_3: 1

        .= ( N-bound ( L~ f)) by A381, A409, A408, GOBOARD7: 6;

        ( mid (f,i1,(( len f) -' 1))) is non empty by A60, A399, SPRECT_2: 7;

        then 1 in ( dom ( mid (f,i1,(( len f) -' 1)))) by FINSEQ_5: 6;

        

        then ((M1 /. 1) `2 ) = ((( mid (f,i1,(( len f) -' 1))) /. 1) `2 ) by FINSEQ_4: 68

        .= ((f /. i1) `2 ) by A60, A399, SPRECT_2: 8

        .= (( S-min ( L~ f)) `2 ) by A398, FINSEQ_5: 38

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

        then

         A415: M1 is_a_v.c._for f by A413, A414, SPRECT_2:def 3;

        

         A416: ( len M1) >= 2 by TOPREAL1:def 8;

        now

          ( NW-corner ( L~ f)) in ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) by RLTOPSP1: 68;

          then ( LSeg (( NW-corner ( L~ f)),A)) c= ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) by A309, A310, TOPREAL1: 6;

          then ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) c= ( L~ ( SpStSeq ( L~ f))) by A66, XBOOLE_1: 1;

          then

           A417: (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ Red2)) c= {u1} by A286, XBOOLE_1: 26;

          assume ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) meets ( L~ Red2);

          then (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ Red2)) <> {} by XBOOLE_0:def 7;

          then (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ Red2)) = {u1} by A417, ZFMISC_1: 33;

          then u1 in (( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) /\ ( L~ Red2)) by TARSKI:def 1;

          then u1 in ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) by XBOOLE_0:def 4;

          then

           A418: u1 in (( LSeg (( NW-corner ( L~ f)),A)) /\ ( LSeg (A,( NE-corner ( L~ f))))) by A381, XBOOLE_0:def 4;

          (( LSeg (( NW-corner ( L~ f)),A)) /\ ( LSeg (A,( NE-corner ( L~ f))))) = {A} by A309, A310, TOPREAL1: 8;

          then u1 = A by A418, TARSKI:def 1;

          hence contradiction by A239, SPRECT_1: 11;

        end;

        then ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) misses ( L~ RB2) by A256, A299, XBOOLE_1: 70;

        then ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) misses (( LSeg ((M4 /. ( len M4)),p2)) \/ ( L~ RB2)) by A132, A401, XBOOLE_1: 70;

        then

         A419: ( LSeg (( NW-corner ( L~ f)),( N-min ( L~ f)))) misses ( L~ M1) by A402, A406, XBOOLE_1: 70;

        ( len M2) >= 2 by TOPREAL1:def 8;

        then

         A420: ( L~ M1) meets ( L~ M2) by A416, A415, A411, SPRECT_2: 29;

        (M3 /. 1) = (f /. 1) by A15, A396, SPRECT_2: 8;

        then ( L~ M3) meets ( L~ M1) by A1, A420, A419, A412, XBOOLE_1: 70;

        then ( L~ M3) meets (( L~ RB2) \/ ( LSeg (p2,(M4 /. ( len M4))))) by A402, A392, XBOOLE_1: 70;

        then ( L~ M3) meets ( L~ RB2) by A401, A393, XBOOLE_1: 70;

        then ( L~ M3) meets ( L~ Red2) by A299, A394, XBOOLE_1: 70;

        then ( L~ M3) meets ( L~ Red) by A251, JORDAN3: 41, XBOOLE_1: 63;

        hence contradiction by A15, A245, A396, SPRECT_3: 18, XBOOLE_1: 63;

      end;

        suppose that

         A421: u1 in ( LSeg (( NE-corner ( L~ f)),( SE-corner ( L~ f)))) and

         A422: ( N-min ( L~ f)) = ( W-max ( L~ f));

        

         A423: ((RB2 /. 1) `1 ) = ( W-bound ( L~ f)) by A96, A298, A422, EUCLID: 52;

        

         A424: (( SE-corner ( L~ f)) `1 ) = ( E-bound ( L~ f)) by EUCLID: 52;

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

        then ((RB2 /. ( len RB2)) `1 ) = ( E-bound ( L~ f)) by A297, A421, A424, GOBOARD7: 5;

        then

         A425: RB2 is_a_h.c._for f by A301, A423, SPRECT_2:def 2;

        set i1 = (( S-max ( L~ f)) .. f), i2 = (( N-max ( L~ f)) .. f), i3 = (( W-min ( L~ f)) .. f);

        

         A426: ( mid (f,i1,i2)) = ( Rev ( mid (f,i2,i1))) by JORDAN4: 18;

        (( N-max ( L~ f)) .. f) <= (( E-max ( L~ f)) .. f) by A1, SPRECT_2: 70;

        then (( N-max ( L~ f)) .. f) < (( E-min ( L~ f)) .. f) by A1, SPRECT_2: 71, XXREAL_0: 2;

        then

         A427: i2 < i1 by A1, SPRECT_2: 72, XXREAL_0: 2;

        ( W-min ( L~ f)) in ( rng f) by SPRECT_2: 43;

        then i3 in ( dom f) by FINSEQ_4: 20;

        then

         A428: i3 <= ( len f) by FINSEQ_3: 25;

        

         A429: 1 < i2 by A1, SPRECT_2: 69;

        

         A430: ( S-max ( L~ f)) in ( rng f) by SPRECT_2: 42;

        then

         A431: i1 in ( dom f) by FINSEQ_4: 20;

        then i1 <= ( len f) by FINSEQ_3: 25;

        then ( mid (f,i2,i1)) is S-Sequence_in_R2 by A429, A427, JORDAN4: 40;

        then

        reconsider M1 = ( mid (f,i1,i2)) as S-Sequence_in_R2 by A426;

        

         A432: ( len RB2) >= 2 by TOPREAL1:def 8;

        (( S-max ( L~ f)) .. f) < (( S-min ( L~ f)) .. f) by A1, SPRECT_2: 73;

        then i3 > i1 by A1, SPRECT_2: 74, XXREAL_0: 2;

        then i1 < ( len f) by A428, XXREAL_0: 2;

        then ( L~ ( mid (f,i2,i1))) misses ( LSeg (u3,p2)) by A257, A429, A427;

        then

         A433: ( L~ M1) misses ( LSeg (u3,p2)) by A426, SPPOL_2: 22;

        

         A434: ( N-max ( L~ f)) in ( rng f) by SPRECT_2: 40;

        then

         A435: i2 in ( dom f) by FINSEQ_4: 20;

        

        then

         A436: ((M1 /. ( len M1)) `2 ) = ((f /. i2) `2 ) by A431, SPRECT_2: 9

        .= (( N-max ( L~ f)) `2 ) by A434, FINSEQ_5: 38

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

        

         A437: M1 is_in_the_area_of f by A431, A435, SPRECT_2: 23;

        ((M1 /. 1) `2 ) = ((f /. i1) `2 ) by A431, A435, SPRECT_2: 8

        .= (( S-max ( L~ f)) `2 ) by A430, FINSEQ_5: 38

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

        then

         A438: M1 is_a_v.c._for f by A437, A436, SPRECT_2:def 3;

        ( len M1) >= 2 by TOPREAL1:def 8;

        then ( L~ M1) meets ( L~ RB2) by A432, A438, A425, SPRECT_2: 29;

        then ( L~ M1) meets ( L~ Red2) by A299, A433, XBOOLE_1: 70;

        then ( L~ M1) meets ( L~ Red) by A251, JORDAN3: 41, XBOOLE_1: 63;

        hence contradiction by A245, A431, A435, SPRECT_3: 18, XBOOLE_1: 63;

      end;

        suppose that

         A439: u1 in ( LSeg (( NE-corner ( L~ f)),( SE-corner ( L~ f)))) and

         A440: ( N-min ( L~ f)) <> ( W-max ( L~ f));

        set i1 = (( S-max ( L~ f)) .. f), i2 = (( N-max ( L~ f)) .. f), i3 = (( W-min ( L~ f)) .. f);

        (( W-max ( L~ f)) .. f) <= (( len f) -' 1) by A1, NAT_D: 49, SPRECT_2: 77;

        then

         A441: i3 < (( len f) -' 1) by A1, A440, SPRECT_2: 75, XXREAL_0: 2;

        

         A442: ( W-min ( L~ f)) in ( rng f) by SPRECT_2: 43;

        then

         A443: i3 in ( dom f) by FINSEQ_4: 20;

        then

         A444: 1 <= i3 by FINSEQ_3: 25;

        then

        reconsider M3 = ( mid (f,i3,(( len f) -' 1))) as S-Sequence_in_R2 by A61, A441, JORDAN4: 39;

        ( L~ M3) misses ( L~ Red) by A60, A245, A443, SPRECT_3: 18, XBOOLE_1: 63;

        then

         A445: ( L~ M3) misses ( L~ Red2) by A251, JORDAN3: 41, XBOOLE_1: 63;

        ( L~ M3) misses ( LSeg (u3,p2)) by A62, A257, A441, A444;

        then

         A446: ( L~ RB2) misses ( L~ M3) by A299, A445, XBOOLE_1: 70;

        

         A447: (M3 /. ( len M3)) = (f /. (( len f) -' 1)) by A60, A443, SPRECT_2: 9;

        then (( LSeg ((M3 /. ( len M3)),p2)) /\ ( L~ M3)) = {(M3 /. ( len M3))} by A126, A441, A444;

        then

        reconsider M2 = (M3 ^ RB2) as S-Sequence_in_R2 by A78, A83, A96, A298, A300, A447, A446, SPRECT_3: 21;

        ( mid (f,i3,(( len f) -' 1))) is_in_the_area_of f by A60, A443, SPRECT_2: 23;

        then

         A448: M2 is_in_the_area_of f by A301, SPRECT_2: 24;

        

         A449: ( mid (f,i1,i2)) = ( Rev ( mid (f,i2,i1))) by JORDAN4: 18;

        

         A450: 1 < i2 by A1, SPRECT_2: 69;

        (( N-max ( L~ f)) .. f) <= (( E-max ( L~ f)) .. f) by A1, SPRECT_2: 70;

        then (( N-max ( L~ f)) .. f) < (( E-min ( L~ f)) .. f) by A1, SPRECT_2: 71, XXREAL_0: 2;

        then

         A451: i2 < i1 by A1, SPRECT_2: 72, XXREAL_0: 2;

        

         A452: ( S-max ( L~ f)) in ( rng f) by SPRECT_2: 42;

        then

         A453: i1 in ( dom f) by FINSEQ_4: 20;

        then i1 <= ( len f) by FINSEQ_3: 25;

        then ( mid (f,i2,i1)) is S-Sequence_in_R2 by A450, A451, JORDAN4: 40;

        then

        reconsider M1 = ( mid (f,i1,i2)) as S-Sequence_in_R2 by A449;

        (( S-max ( L~ f)) .. f) < (( S-min ( L~ f)) .. f) by A1, SPRECT_2: 73;

        then

         A454: i3 > i1 by A1, SPRECT_2: 74, XXREAL_0: 2;

        then

         A455: ( L~ M1) misses ( L~ M3) by A62, A450, A451, A441, SPRECT_2: 50;

        i3 < ( len f) by A61, A441, NAT_1: 13;

        then i1 < ( len f) by A454, XXREAL_0: 2;

        then ( L~ ( mid (f,i2,i1))) misses ( LSeg (u3,p2)) by A257, A450, A451;

        then

         A456: ( L~ M1) misses ( LSeg (u3,p2)) by A449, SPPOL_2: 22;

        

         A457: ( len M1) >= 2 by TOPREAL1:def 8;

        

         A458: ( N-max ( L~ f)) in ( rng f) by SPRECT_2: 40;

        then

         A459: i2 in ( dom f) by FINSEQ_4: 20;

        

        then

         A460: ((M1 /. ( len M1)) `2 ) = ((f /. i2) `2 ) by A453, SPRECT_2: 9

        .= (( N-max ( L~ f)) `2 ) by A458, FINSEQ_5: 38

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

        i1 < (( len f) -' 1) by A454, A441, XXREAL_0: 2;

        then ( L~ ( mid (f,i2,i1))) misses ( LSeg (p2,(f /. (( len f) -' 1)))) by A105, A450, A451;

        then

         A461: ( L~ M1) misses ( LSeg (p2,(f /. (( len f) -' 1)))) by A449, SPPOL_2: 22;

        

         A462: (( SE-corner ( L~ f)) `1 ) = ( E-bound ( L~ f)) by EUCLID: 52;

        

         A463: (( NE-corner ( L~ f)) `1 ) = ( E-bound ( L~ f)) by EUCLID: 52;

        

         A464: ((M2 /. ( len M2)) `1 ) = ((RB2 /. ( len RB2)) `1 ) by SPRECT_3: 1

        .= ( E-bound ( L~ f)) by A297, A439, A463, A462, GOBOARD7: 5;

        ( mid (f,i3,(( len f) -' 1))) is non empty by A60, A443, SPRECT_2: 7;

        then 1 in ( dom ( mid (f,i3,(( len f) -' 1)))) by FINSEQ_5: 6;

        

        then ((M2 /. 1) `1 ) = ((( mid (f,i3,(( len f) -' 1))) /. 1) `1 ) by FINSEQ_4: 68

        .= ((f /. i3) `1 ) by A60, A443, SPRECT_2: 8

        .= (( W-min ( L~ f)) `1 ) by A442, FINSEQ_5: 38

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

        then

         A465: M2 is_a_h.c._for f by A448, A464, SPRECT_2:def 2;

        

         A466: ( L~ M2) = ((( L~ M3) \/ ( LSeg ((M3 /. ( len M3)),p2))) \/ ( L~ RB2)) by A298, SPPOL_2: 23

        .= (( L~ M3) \/ (( LSeg ((M3 /. ( len M3)),p2)) \/ ( L~ RB2))) by XBOOLE_1: 4;

        

         A467: M1 is_in_the_area_of f by A453, A459, SPRECT_2: 23;

        ((M1 /. 1) `2 ) = ((f /. i1) `2 ) by A453, A459, SPRECT_2: 8

        .= (( S-max ( L~ f)) `2 ) by A452, FINSEQ_5: 38

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

        then

         A468: M1 is_a_v.c._for f by A467, A460, SPRECT_2:def 3;

        ( len M2) >= 2 by TOPREAL1:def 8;

        then ( L~ M1) meets ( L~ M2) by A457, A468, A465, SPRECT_2: 29;

        then ( L~ M1) meets (( L~ RB2) \/ ( LSeg (p2,(M3 /. ( len M3))))) by A466, A455, XBOOLE_1: 70;

        then ( L~ M1) meets ( L~ RB2) by A447, A461, XBOOLE_1: 70;

        then ( L~ M1) meets ( L~ Red2) by A299, A456, XBOOLE_1: 70;

        then ( L~ M1) meets ( L~ Red) by A251, JORDAN3: 41, XBOOLE_1: 63;

        hence contradiction by A245, A453, A459, SPRECT_3: 18, XBOOLE_1: 63;

      end;

        suppose

         A469: u1 in ( LSeg (( SE-corner ( L~ f)),( SW-corner ( L~ f))));

        

         A470: (( SW-corner ( L~ f)) `2 ) = ( S-bound ( L~ f)) by EUCLID: 52;

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

        then ((RB1 /. 1) `2 ) = ( S-bound ( L~ f)) by A302, A469, A470, GOBOARD7: 6;

        then

         A471: RB1 is_a_v.c._for f by A170, A303, A306, SPRECT_2:def 3;

        

         A472: ( len RB1) >= 2 by TOPREAL1:def 8;

        set i1 = (( E-min ( L~ f)) .. f), i2 = (( W-min ( L~ f)) .. f);

        

         A473: ( mid (f,i2,i1)) = ( Rev ( mid (f,i1,i2))) by JORDAN4: 18;

        (( E-min ( L~ f)) .. f) <= (( S-max ( L~ f)) .. f) by A1, SPRECT_2: 72;

        then (( E-min ( L~ f)) .. f) < (( S-min ( L~ f)) .. f) by A1, SPRECT_2: 73, XXREAL_0: 2;

        then

         A474: i1 < i2 by A1, SPRECT_2: 74, XXREAL_0: 2;

        (( N-max ( L~ f)) .. f) > 1 by A1, SPRECT_2: 69;

        then (( E-max ( L~ f)) .. f) > 1 by A1, SPRECT_2: 70, XXREAL_0: 2;

        then

         A475: 1 < i1 by A1, SPRECT_2: 71, XXREAL_0: 2;

        

         A476: ( W-min ( L~ f)) in ( rng f) by SPRECT_2: 43;

        then

         A477: i2 in ( dom f) by FINSEQ_4: 20;

        then

         A478: i2 <= ( len f) by FINSEQ_3: 25;

        then ( mid (f,i1,i2)) is S-Sequence_in_R2 by A475, A474, JORDAN4: 40;

        then

        reconsider M2 = ( mid (f,i2,i1)) as S-Sequence_in_R2 by A473;

        ( L~ ( mid (f,i1,i2))) misses ( LSeg (u2,p1)) by A270, A475, A474, A478;

        then

         A479: ( L~ M2) misses ( LSeg (u2,p1)) by A473, SPPOL_2: 22;

        

         A480: ( E-min ( L~ f)) in ( rng f) by SPRECT_2: 45;

        then

         A481: i1 in ( dom f) by FINSEQ_4: 20;

        then

         A482: M2 is_in_the_area_of f by A477, SPRECT_2: 23;

        

         A483: ((M2 /. 1) `1 ) = ((f /. i2) `1 ) by A481, A477, SPRECT_2: 8

        .= (( W-min ( L~ f)) `1 ) by A476, FINSEQ_5: 38

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

        ((M2 /. ( len M2)) `1 ) = ((f /. i1) `1 ) by A481, A477, SPRECT_2: 9

        .= (( E-min ( L~ f)) `1 ) by A480, FINSEQ_5: 38

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

        then

         A484: M2 is_a_h.c._for f by A482, A483, SPRECT_2:def 2;

        ( len M2) >= 2 by TOPREAL1:def 8;

        then ( L~ RB1) meets ( L~ M2) by A472, A471, A484, SPRECT_2: 29;

        then ( L~ M2) meets ( L~ Red1) by A304, A479, XBOOLE_1: 70;

        then ( L~ M2) meets ( L~ Red) by A264, JORDAN3: 41, XBOOLE_1: 63;

        hence contradiction by A245, A481, A477, SPRECT_3: 18, XBOOLE_1: 63;

      end;

        suppose

         A485: u1 in ( LSeg (( SW-corner ( L~ f)),( NW-corner ( L~ f))));

        

         A486: (( SW-corner ( L~ f)) `1 ) = ( W-bound ( L~ f)) by EUCLID: 52;

        set i1 = (( S-min ( L~ f)) .. f), i3 = (( E-min ( L~ f)) .. f);

        

         A487: (( NW-corner ( L~ f)) `1 ) = ( W-bound ( L~ f)) by EUCLID: 52;

        (( N-max ( L~ f)) .. f) > 1 by A1, SPRECT_2: 69;

        then (( E-max ( L~ f)) .. f) > 1 by A1, SPRECT_2: 70, XXREAL_0: 2;

        then (( E-max ( L~ f)) .. f) >= (1 + 1) by NAT_1: 13;

        then

         A488: 2 < i3 by A1, SPRECT_2: 71, XXREAL_0: 2;

        

         A489: ( E-min ( L~ f)) in ( rng f) by SPRECT_2: 45;

        then

         A490: i3 in ( dom f) by FINSEQ_4: 20;

        then

         A491: i3 <= ( len f) by FINSEQ_3: 25;

        then

        reconsider M3 = ( mid (f,2,i3)) as S-Sequence_in_R2 by A488, JORDAN4: 40;

        ( L~ M3) misses ( L~ Red) by A57, A245, A490, SPRECT_3: 18, XBOOLE_1: 63;

        then

         A492: ( L~ M3) misses ( L~ Red1) by A264, JORDAN3: 41, XBOOLE_1: 63;

        ( L~ M3) misses ( LSeg (u2,p1)) by A270, A488, A491;

        then

         A493: ( L~ RB1) misses ( L~ M3) by A304, A492, XBOOLE_1: 70;

        

         A494: (M3 /. 1) = (f /. 2) by A57, A490, SPRECT_2: 8;

        then (( LSeg (p1,(M3 /. 1))) /\ ( L~ M3)) = {(M3 /. 1)} by A191, A488, A491;

        then

        reconsider M2 = (RB1 ^ M3) as S-Sequence_in_R2 by A80, A170, A303, A305, A494, A493, SPRECT_3: 21;

        

         A495: ((M2 /. ( len M2)) `1 ) = ((( mid (f,2,i3)) /. ( len ( mid (f,2,i3)))) `1 ) by SPRECT_3: 1

        .= ((f /. i3) `1 ) by A57, A490, SPRECT_2: 9

        .= (( E-min ( L~ f)) `1 ) by A489, FINSEQ_5: 38

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

        ( mid (f,2,i3)) is_in_the_area_of f by A57, A490, SPRECT_2: 23;

        then

         A496: M2 is_in_the_area_of f by A306, SPRECT_2: 24;

        1 in ( dom RB1) by FINSEQ_5: 6;

        

        then ((M2 /. 1) `1 ) = ((RB1 /. 1) `1 ) by FINSEQ_4: 68

        .= ( W-bound ( L~ f)) by A302, A485, A487, A486, GOBOARD7: 5;

        then

         A497: M2 is_a_h.c._for f by A496, A495, SPRECT_2:def 2;

        

         A498: ( L~ M2) = ((( L~ RB1) \/ ( LSeg (p1,(M3 /. 1)))) \/ ( L~ M3)) by A303, SPPOL_2: 23;

        (( W-min ( L~ f)) .. f) < ( len f) by A1, SPRECT_2: 76;

        then

         A499: i1 < ( len f) by A1, SPRECT_2: 74, XXREAL_0: 2;

        (( E-min ( L~ f)) .. f) <= (( S-max ( L~ f)) .. f) by A1, SPRECT_2: 72;

        then

         A500: i3 < i1 by A1, SPRECT_2: 73, XXREAL_0: 2;

        then

         A501: 2 < i1 by A488, XXREAL_0: 2;

        then

         A502: 1 < i1 by XXREAL_0: 2;

        then

        reconsider M1 = ( mid (f,i1,( len f))) as S-Sequence_in_R2 by A499, JORDAN4: 40;

        

         A503: ( L~ M1) misses ( L~ M3) by A500, A499, A488, SPRECT_2: 47;

        

         A504: ( L~ M1) misses ( LSeg (p1,(f /. 2))) by A173, A499, A501;

        

         A505: ( S-min ( L~ f)) in ( rng f) by SPRECT_2: 41;

        then

         A506: i1 in ( dom f) by FINSEQ_4: 20;

        then

         A507: M1 is_in_the_area_of f by A58, SPRECT_2: 23;

        

         A508: ((M1 /. ( len M1)) `2 ) = ((f /. ( len f)) `2 ) by A58, A506, SPRECT_2: 9

        .= ((f /. 1) `2 ) by FINSEQ_6:def 1

        .= ( N-bound ( L~ f)) by A1, EUCLID: 52;

        ((M1 /. 1) `2 ) = ((f /. i1) `2 ) by A58, A506, SPRECT_2: 8

        .= (( S-min ( L~ f)) `2 ) by A505, FINSEQ_5: 38

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

        then

         A509: M1 is_a_v.c._for f by A507, A508, SPRECT_2:def 3;

        

         A510: ( L~ M1) misses ( LSeg (u2,p1)) by A270, A499, A502;

        

         A511: ( len M1) >= 2 by TOPREAL1:def 8;

        ( len M2) >= 2 by TOPREAL1:def 8;

        then ( L~ M1) meets ( L~ M2) by A511, A509, A497, SPRECT_2: 29;

        then ( L~ M1) meets (( L~ RB1) \/ ( LSeg (p1,(M3 /. 1)))) by A498, A503, XBOOLE_1: 70;

        then ( L~ M1) meets ( L~ RB1) by A494, A504, XBOOLE_1: 70;

        then ( L~ M1) meets ( L~ Red1) by A304, A510, XBOOLE_1: 70;

        then ( L~ M1) meets ( L~ Red) by A264, JORDAN3: 41, XBOOLE_1: 63;

        hence contradiction by A58, A245, A506, SPRECT_3: 18, XBOOLE_1: 63;

      end;

    end;

    

     Lm2: for f be non constant standard special_circular_sequence st (f /. 1) = ( N-min ( L~ f)) holds ( LeftComp f) <> ( RightComp f)

    proof

      let f be non constant standard special_circular_sequence such that

       A1: (f /. 1) = ( N-min ( L~ f));

      per cases by REVROT_1: 38;

        suppose f is clockwise_oriented;

        hence thesis by A1, Lm1;

      end;

        suppose

         A2: ( Rev f) is clockwise_oriented;

        

         A3: ( LeftComp ( Rev f)) = ( RightComp f) by GOBOARD9: 23;

        

         A4: ( RightComp ( Rev f)) = ( LeftComp f) by GOBOARD9: 24;

        ( N-min ( L~ ( Rev f))) = ( N-min ( L~ f)) by SPPOL_2: 22

        .= (( Rev f) /. ( len f)) by A1, FINSEQ_5: 65

        .= (( Rev f) /. ( len ( Rev f))) by FINSEQ_5:def 3

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

        hence thesis by A2, A3, A4, Lm1;

      end;

    end;

    theorem :: SPRECT_4:6

    for f be non constant standard special_circular_sequence holds ( LeftComp f) <> ( RightComp f)

    proof

      let f be non constant standard special_circular_sequence;

      set g = ( Rotate (f,( N-min ( L~ f))));

      

       A1: ( L~ f) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ f)) in ( rng f) by SPRECT_2: 39;

      then

       A2: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      

       A3: ( RightComp g) = ( RightComp f) by REVROT_1: 37;

      ( LeftComp g) = ( LeftComp f) by REVROT_1: 36;

      hence thesis by A2, A3, Lm2;

    end;