sprect_3.miz



    begin

    theorem :: SPRECT_3:1

    for D be non empty set holds for f be non empty FinSequence of D, g be FinSequence of D holds ((g ^ f) /. ( len (g ^ f))) = (f /. ( len f))

    proof

      let D be non empty set, f be non empty FinSequence of D, g be FinSequence of D;

      

       A1: ( len f) >= 1 by NAT_1: 14;

      ( len (g ^ f)) = (( len g) + ( len f)) by FINSEQ_1: 22;

      hence thesis by A1, SEQ_4: 136;

    end;

    theorem :: SPRECT_3:2

    

     Th2: for a,b,c,d be set holds ( Indices ((a,b) ][ (c,d))) = { [1, 1], [1, 2], [2, 1], [2, 2]}

    proof

      let a,b,c,d be set;

      

      thus ( Indices ((a,b) ][ (c,d))) = [:( Seg 2), ( Seg 2):] by MATRIX_0: 47

      .= ( [: {1}, ( Seg 2):] \/ [: {2}, ( Seg 2):]) by FINSEQ_1: 2, ZFMISC_1: 109

      .= ( [: {1}, ( Seg 2):] \/ { [2, 1], [2, 2]}) by FINSEQ_1: 2, ZFMISC_1: 30

      .= ( { [1, 1], [1, 2]} \/ { [2, 1], [2, 2]}) by FINSEQ_1: 2, ZFMISC_1: 30

      .= { [1, 1], [1, 2], [2, 1], [2, 2]} by ENUMSET1: 5;

    end;

    begin

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

    theorem :: SPRECT_3:3

    

     Th3: for p,q be Point of ( TOP-REAL n), r be Real st 0 < r & p = (((1 - r) * p) + (r * q)) holds p = q

    proof

      let p,q be Point of ( TOP-REAL n), r be Real such that

       A1: 0 < r and

       A2: p = (((1 - r) * p) + (r * q));

      

       A3: (((1 - r) * p) + (r * p)) = (((1 - r) + r) * p) by RLVECT_1:def 6

      .= p by RLVECT_1:def 8;

      (r * p) = ((r * p) + ( 0. ( TOP-REAL n))) by RLVECT_1: 4

      .= ((r * p) + (((1 - r) * p) + ( - ((1 - r) * p)))) by RLVECT_1: 5

      .= (((r * q) + ((1 - r) * p)) + ( - ((1 - r) * p))) by A2, A3, RLVECT_1:def 3

      .= ((r * q) + (((1 - r) * p) + ( - ((1 - r) * p)))) by RLVECT_1:def 3

      .= ((r * q) + ( 0. ( TOP-REAL n))) by RLVECT_1: 5

      .= (r * q) by RLVECT_1: 4;

      hence thesis by A1, RLVECT_1: 36;

    end;

    theorem :: SPRECT_3:4

    

     Th4: for p,q be Point of ( TOP-REAL n), r be Real st r < 1 & p = (((1 - r) * q) + (r * p)) holds p = q

    proof

      let p,q be Point of ( TOP-REAL n), r be Real such that

       A1: r < 1 and

       A2: p = (((1 - r) * q) + (r * p));

      set s = (1 - r);

      (r + 0 ) < 1 by A1;

      then

       A3: 0 < (1 - r) by XREAL_1: 20;

      p = (((1 - s) * p) + (s * q)) by A2;

      hence thesis by A3, Th3;

    end;

    theorem :: SPRECT_3:5

    for p,q be Point of ( TOP-REAL n) st p = ((1 / 2) * (p + q)) holds p = q

    proof

      let p,q be Point of ( TOP-REAL n);

      assume p = ((1 / 2) * (p + q));

      then p = (((1 - (1 / 2)) * p) + ((1 / 2) * q)) by RLVECT_1:def 5;

      hence thesis by Th3;

    end;

    theorem :: SPRECT_3:6

    

     Th6: for p,q,r be Point of ( TOP-REAL n) st q in ( LSeg (p,r)) & r in ( LSeg (p,q)) holds q = r

    proof

      let p,q,r be Point of ( TOP-REAL n);

      assume q in ( LSeg (p,r));

      then

      consider r1 be Real such that

       A1: q = (((1 - r1) * p) + (r1 * r)) and

       A2: 0 <= r1 and

       A3: r1 <= 1;

      assume r in ( LSeg (p,q));

      then

      consider r2 be Real such that

       A4: r = (((1 - r2) * p) + (r2 * q)) and 0 <= r2 and

       A5: r2 <= 1;

      

       A6: (r1 * r2) <= 1 by A2, A3, A5, XREAL_1: 160;

      

       A7: ((1 - r2) + (r2 * (1 - r1))) = (1 - (r2 * r1));

      

       A8: r = (((1 - r2) * p) + ((r2 * ((1 - r1) * p)) + (r2 * (r1 * r)))) by A1, A4, RLVECT_1:def 5

      .= ((((1 - r2) * p) + (r2 * ((1 - r1) * p))) + (r2 * (r1 * r))) by RLVECT_1:def 3

      .= ((((1 - r2) * p) + ((r2 * (1 - r1)) * p)) + (r2 * (r1 * r))) by RLVECT_1:def 7

      .= (((1 - (r2 * r1)) * p) + (r2 * (r1 * r))) by A7, RLVECT_1:def 6

      .= (((1 - (r2 * r1)) * p) + ((r2 * r1) * r)) by RLVECT_1:def 7;

      

       A9: ((1 - r1) + (r1 * (1 - r2))) = (1 - (r1 * r2));

      

       A10: q = (((1 - r1) * p) + ((r1 * ((1 - r2) * p)) + (r1 * (r2 * q)))) by A1, A4, RLVECT_1:def 5

      .= ((((1 - r1) * p) + (r1 * ((1 - r2) * p))) + (r1 * (r2 * q))) by RLVECT_1:def 3

      .= ((((1 - r1) * p) + ((r1 * (1 - r2)) * p)) + (r1 * (r2 * q))) by RLVECT_1:def 7

      .= (((1 - (r1 * r2)) * p) + (r1 * (r2 * q))) by A9, RLVECT_1:def 6

      .= (((1 - (r1 * r2)) * p) + ((r1 * r2) * q)) by RLVECT_1:def 7;

      per cases by A6, XXREAL_0: 1;

        suppose

         A11: (r1 * r2) = 1;

        then 1 <= r1 or 1 <= r2 by A2, XREAL_1: 162;

        then (1 * r1) = 1 or (1 * r2) = 1 by A3, A5, XXREAL_0: 1;

        

        hence q = (( 0 * p) + r) by A1, A11, RLVECT_1:def 8

        .= (( 0. ( TOP-REAL n)) + r) by RLVECT_1: 10

        .= r by RLVECT_1: 4;

      end;

        suppose

         A12: (r1 * r2) < 1;

        

        hence q = p by A10, Th4

        .= r by A8, A12, Th4;

      end;

    end;

    begin

    theorem :: SPRECT_3:7

    

     Th7: for A be non empty Subset of ( TOP-REAL 2), p be Element of ( Euclid 2), r be Real st A = ( Ball (p,r)) holds A is connected

    proof

      let A be non empty Subset of ( TOP-REAL 2), p be Element of ( Euclid 2), r be Real such that

       A1: A = ( Ball (p,r));

      A is convex by A1, TOPREAL3: 21;

      hence thesis;

    end;

    theorem :: SPRECT_3:8

    

     Th8: for A,B be Subset of ( TOP-REAL 2) st A is open & B is_a_component_of A holds B is open

    proof

      let A,B be Subset of ( TOP-REAL 2) such that

       A1: A is open and

       A2: B is_a_component_of A;

      

       A3: B c= A by A2, SPRECT_1: 5;

      

       A4: the TopStruct of ( TOP-REAL 2) = ( TopSpaceMetr ( Euclid 2)) by EUCLID:def 8;

      then

      reconsider C = B, D = A as Subset of ( TopSpaceMetr ( Euclid 2));

      

       A5: D is open by A1, A4, PRE_TOPC: 30;

      for p be Point of ( Euclid 2) st p in C holds ex r be Real st r > 0 & ( Ball (p,r)) c= C

      proof

        let p be Point of ( Euclid 2);

        assume

         A6: p in C;

        then

        consider r be Real such that

         A7: r > 0 and

         A8: ( Ball (p,r)) c= D by A3, A5, TOPMETR: 15;

        reconsider r as Real;

        take r;

        thus r > 0 by A7;

        reconsider E = ( Ball (p,r)) as Subset of ( TOP-REAL 2) by A4, TOPMETR: 12;

        

         A9: p in E by A7, GOBOARD6: 1;

        then

         A10: E is connected by Th7;

        B meets E by A6, A9, XBOOLE_0: 3;

        hence thesis by A2, A8, A10, GOBOARD9: 4;

      end;

      then C is open by TOPMETR: 15;

      hence B is open by A4, PRE_TOPC: 30;

    end;

    theorem :: SPRECT_3:9

    for p,q,r,s be Point of ( TOP-REAL 2) st ( LSeg (p,q)) is horizontal & ( LSeg (r,s)) is horizontal & ( LSeg (p,q)) meets ( LSeg (r,s)) holds (p `2 ) = (r `2 )

    proof

      let p,q,r,s be Point of ( TOP-REAL 2) such that

       A1: ( LSeg (p,q)) is horizontal and

       A2: ( LSeg (r,s)) is horizontal;

      assume ( LSeg (p,q)) meets ( LSeg (r,s));

      then (( LSeg (p,q)) /\ ( LSeg (r,s))) <> {} ;

      then

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

       A3: x in (( LSeg (p,q)) /\ ( LSeg (r,s))) by SUBSET_1: 4;

      

       A4: x in ( LSeg (r,s)) by A3, XBOOLE_0:def 4;

      x in ( LSeg (p,q)) by A3, XBOOLE_0:def 4;

      

      hence (p `2 ) = (x `2 ) by A1, SPPOL_1: 40

      .= (r `2 ) by A2, A4, SPPOL_1: 40;

    end;

    theorem :: SPRECT_3:10

    for p,q,r be Point of ( TOP-REAL 2) st ( LSeg (p,q)) is vertical & ( LSeg (q,r)) is horizontal holds (( LSeg (p,q)) /\ ( LSeg (q,r))) = {q}

    proof

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

       A1: ( LSeg (p,q)) is vertical and

       A2: ( LSeg (q,r)) is horizontal;

      for x be object holds x in (( LSeg (p,q)) /\ ( LSeg (q,r))) iff x = q

      proof

        let x be object;

        thus x in (( LSeg (p,q)) /\ ( LSeg (q,r))) implies x = q

        proof

          assume

           A3: x in (( LSeg (p,q)) /\ ( LSeg (q,r)));

          then

          reconsider x as Point of ( TOP-REAL 2);

          x in ( LSeg (q,r)) by A3, XBOOLE_0:def 4;

          then

           A4: (x `2 ) = (q `2 ) by A2, SPPOL_1: 40;

          x in ( LSeg (p,q)) by A3, XBOOLE_0:def 4;

          then (x `1 ) = (q `1 ) by A1, SPPOL_1: 41;

          hence thesis by A4, TOPREAL3: 6;

        end;

        assume

         A5: x = q;

        then

         A6: x in ( LSeg (q,r)) by RLTOPSP1: 68;

        x in ( LSeg (p,q)) by A5, RLTOPSP1: 68;

        hence thesis by A6, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: SPRECT_3:11

    for p,q,r,s be Point of ( TOP-REAL 2) st ( LSeg (p,q)) is horizontal & ( LSeg (s,r)) is vertical & r in ( LSeg (p,q)) holds (( LSeg (p,q)) /\ ( LSeg (s,r))) = {r}

    proof

      let p,q,r,s be Point of ( TOP-REAL 2) such that

       A1: ( LSeg (p,q)) is horizontal and

       A2: ( LSeg (s,r)) is vertical and

       A3: r in ( LSeg (p,q));

      for x be object holds x in (( LSeg (p,q)) /\ ( LSeg (s,r))) iff x = r

      proof

        let x be object;

        thus x in (( LSeg (p,q)) /\ ( LSeg (s,r))) implies x = r

        proof

          assume

           A4: x in (( LSeg (p,q)) /\ ( LSeg (s,r)));

          then

          reconsider x as Point of ( TOP-REAL 2);

          x in ( LSeg (p,q)) by A4, XBOOLE_0:def 4;

          then

           A5: (x `2 ) = (p `2 ) by A1, SPPOL_1: 40;

          x in ( LSeg (s,r)) by A4, XBOOLE_0:def 4;

          then

           A6: (x `1 ) = (r `1 ) by A2, SPPOL_1: 41;

          (p `2 ) = (r `2 ) by A1, A3, SPPOL_1: 40;

          hence thesis by A5, A6, TOPREAL3: 6;

        end;

        assume

         A7: x = r;

        then x in ( LSeg (s,r)) by RLTOPSP1: 68;

        hence thesis by A3, A7, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    begin

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

    reserve G for Go-board;

    theorem :: SPRECT_3:12

    1 <= j & j <= k & k <= ( width G) & 1 <= i & i <= ( len G) implies ((G * (i,j)) `2 ) <= ((G * (i,k)) `2 )

    proof

      assume that

       A1: 1 <= j and

       A2: j <= k and

       A3: k <= ( width G) and

       A4: 1 <= i and

       A5: i <= ( len G);

      per cases by A2, XXREAL_0: 1;

        suppose j < k;

        hence thesis by A1, A3, A4, A5, GOBOARD5: 4;

      end;

        suppose j = k;

        hence thesis;

      end;

    end;

    theorem :: SPRECT_3:13

    1 <= j & j <= ( width G) & 1 <= i & i <= k & k <= ( len G) implies ((G * (i,j)) `1 ) <= ((G * (k,j)) `1 )

    proof

      assume that

       A1: 1 <= j and

       A2: j <= ( width G) and

       A3: 1 <= i and

       A4: i <= k and

       A5: k <= ( len G);

      per cases by A4, XXREAL_0: 1;

        suppose i < k;

        hence thesis by A1, A2, A3, A5, GOBOARD5: 3;

      end;

        suppose i = k;

        hence thesis;

      end;

    end;

    reserve C for Subset of ( TOP-REAL 2);

    theorem :: SPRECT_3:14

    

     Th14: ( LSeg (( NW-corner C),( NE-corner C))) c= ( L~ ( SpStSeq C))

    proof

      

       A1: (( LSeg (( NW-corner C),( NE-corner C))) \/ ( LSeg (( NE-corner C),( SE-corner C)))) c= ((( LSeg (( NW-corner C),( NE-corner C))) \/ ( LSeg (( NE-corner C),( SE-corner C)))) \/ (( LSeg (( SE-corner C),( SW-corner C))) \/ ( LSeg (( SW-corner C),( NW-corner C))))) by XBOOLE_1: 7;

      ( LSeg (( NW-corner C),( NE-corner C))) c= (( LSeg (( NW-corner C),( NE-corner C))) \/ ( LSeg (( NE-corner C),( SE-corner C)))) by XBOOLE_1: 7;

      then ( LSeg (( NW-corner C),( NE-corner C))) c= ((( LSeg (( NW-corner C),( NE-corner C))) \/ ( LSeg (( NE-corner C),( SE-corner C)))) \/ (( LSeg (( SE-corner C),( SW-corner C))) \/ ( LSeg (( SW-corner C),( NW-corner C))))) by A1;

      hence thesis by SPRECT_1: 41;

    end;

    theorem :: SPRECT_3:15

    

     Th15: for C be non empty compact Subset of ( TOP-REAL 2) holds ( N-min C) in ( LSeg (( NW-corner C),( NE-corner C)))

    proof

      let C be non empty compact Subset of ( TOP-REAL 2);

      

       A1: ( N-most C) c= ( LSeg (( NW-corner C),( NE-corner C))) by XBOOLE_1: 17;

      ( N-min C) in ( N-most C) by PSCOMP_1: 42;

      hence thesis by A1;

    end;

    registration

      let C;

      cluster ( LSeg (( NW-corner C),( NE-corner C))) -> horizontal;

      coherence

      proof

        (( NW-corner C) `2 ) = ( N-bound C) by EUCLID: 52

        .= (( NE-corner C) `2 ) by EUCLID: 52;

        hence thesis by SPPOL_1: 15;

      end;

    end

    theorem :: SPRECT_3:16

    for g be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st (g /. 1) <> p & (((g /. 1) `1 ) = (p `1 ) or ((g /. 1) `2 ) = (p `2 )) & g is being_S-Seq & (( LSeg (p,(g /. 1))) /\ ( L~ g)) = {(g /. 1)} holds ( <*p*> ^ g) is being_S-Seq

    proof

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

       A1: (g /. 1) <> p and

       A2: ((g /. 1) `1 ) = (p `1 ) or ((g /. 1) `2 ) = (p `2 ) and

       A3: g is being_S-Seq and

       A4: (( LSeg (p,(g /. 1))) /\ ( L~ g)) = {(g /. 1)};

      set f = <*p, (g /. 1)*>;

      

       A5: f is being_S-Seq by A1, A2, SPPOL_2: 43;

      reconsider g9 = g as S-Sequence_in_R2 by A3;

      

       A6: 1 in ( dom g9) by FINSEQ_5: 6;

      

       A7: ( len f) = (1 + 1) by FINSEQ_1: 44;

      then

       AB: (( len f) -' 1) = 1 by NAT_D: 34;

      

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

      

      then

       A8: ( mid (f,1,(( len f) -' 1))) = <*(f . 1)*> by AB, JORDAN4: 15

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

      .= <*p*> by FINSEQ_4: 17;

      

       A9: (( L~ f) /\ ( L~ g)) = {(g /. 1)} by A4, SPPOL_2: 21

      .= {(g . 1)} by A6, PARTFUN1:def 6;

      (f . ( len f)) = (g /. 1) by A7, FINSEQ_1: 44

      .= (g . 1) by A6, PARTFUN1:def 6;

      hence thesis by A3, A5, A9, A8, JORDAN3: 45;

    end;

    theorem :: SPRECT_3:17

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

    proof

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

       A1: 1 < j and

       A2: j <= ( len f) and

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

      consider i such that

       A4: 1 <= i and

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

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

      

       A7: ((j -' 1) + 1) = j by A1, XREAL_1: 235;

      then

       A8: (i + 1) <= j by A1, A2, A5, JORDAN4: 8;

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

      then

       A9: ( LSeg (( mid (f,1,j)),i)) = ( LSeg (f,((i + 1) -' 1))) by A1, A2, A4, JORDAN4: 19;

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

      then

       A10: LE ((f /. (i + 1)),(f /. j),( L~ f),(f /. 1),(f /. ( len f))) by A2, A8, JORDAN5C: 24;

      

       A11: i = ((i + 1) -' 1) by NAT_D: 34;

      (i + 1) <= ( len f) by A2, A8, XXREAL_0: 2;

      then LE (p,(f /. (i + 1)),( L~ f),(f /. 1),(f /. ( len f))) by A4, A6, A11, A9, JORDAN5C: 26;

      hence thesis by A10, JORDAN5C: 13;

    end;

    theorem :: SPRECT_3:18

    for h be FinSequence of ( TOP-REAL 2) st i in ( dom h) & j in ( dom h) holds ( L~ ( mid (h,i,j))) c= ( L~ h)

    proof

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

      assume that

       A1: i in ( dom h) and

       A2: j in ( dom h);

      

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

      

       A4: j <= ( len h) by A2, FINSEQ_3: 25;

      

       A5: 1 <= j by A2, FINSEQ_3: 25;

      1 <= i by A1, FINSEQ_3: 25;

      hence thesis by A3, A5, A4, JORDAN4: 35;

    end;

    theorem :: SPRECT_3:19

    1 <= i & i < j implies for f be FinSequence of ( TOP-REAL 2) st j <= ( len f) holds ( L~ ( mid (f,i,j))) = (( LSeg (f,i)) \/ ( L~ ( mid (f,(i + 1),j))))

    proof

      assume that

       A1: 1 <= i and

       A2: i < j;

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

       A3: j <= ( len f);

      set A = { ( LSeg (f,k)) : i <= k & k < j }, B = { ( LSeg (f,k)) : (i + 1) <= k & k < j };

      

       A4: A = (B \/ {( LSeg (f,i))})

      proof

        thus A c= (B \/ {( LSeg (f,i))})

        proof

          let e be object;

          assume e in A;

          then

          consider k such that

           A5: e = ( LSeg (f,k)) and

           A6: i <= k and

           A7: k < j;

          i = k or i < k by A6, XXREAL_0: 1;

          then i = k or (i + 1) <= k by NAT_1: 13;

          then e in B or e in {( LSeg (f,i))} by A5, A7, TARSKI:def 1;

          hence thesis by XBOOLE_0:def 3;

        end;

        let e be object;

        assume

         A8: e in (B \/ {( LSeg (f,i))});

        per cases by A8, XBOOLE_0:def 3;

          suppose e in B;

          then

          consider k such that

           A9: e = ( LSeg (f,k)) and

           A10: (i + 1) <= k and

           A11: k < j;

          i < k by A10, NAT_1: 13;

          hence thesis by A9, A11;

        end;

          suppose e in {( LSeg (f,i))};

          then e = ( LSeg (f,i)) by TARSKI:def 1;

          hence thesis by A2;

        end;

      end;

      

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

      

       A13: (i + 1) <= j by A2, NAT_1: 13;

      

      thus ( L~ ( mid (f,i,j))) = ( union A) by A1, A2, A3, SPRECT_2: 14

      .= (( union B) \/ ( union {( LSeg (f,i))})) by A4, ZFMISC_1: 78

      .= (( union B) \/ ( LSeg (f,i))) by ZFMISC_1: 25

      .= (( LSeg (f,i)) \/ ( L~ ( mid (f,(i + 1),j)))) by A3, A12, A13, SPRECT_2: 14;

    end;

    theorem :: SPRECT_3:20

    for f be FinSequence of ( TOP-REAL 2) st 1 <= i holds i < j & j <= ( len f) implies ( L~ ( mid (f,i,j))) = (( L~ ( mid (f,i,(j -' 1)))) \/ ( LSeg (f,(j -' 1))))

    proof

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

       A1: 1 <= i and

       A2: i < j and

       A3: j <= ( len f);

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

      then

       A4: (j -' 1) <= ( len f) by A3, XXREAL_0: 2;

      set A = { ( LSeg (f,k)) : i <= k & k < j }, B = { ( LSeg (f,k)) : i <= k & k < (j -' 1) };

      

       A5: i <= (j -' 1) by A2, NAT_D: 49;

      

       A6: A = (B \/ {( LSeg (f,(j -' 1)))})

      proof

        thus A c= (B \/ {( LSeg (f,(j -' 1)))})

        proof

          let e be object;

          assume e in A;

          then

          consider k such that

           A7: e = ( LSeg (f,k)) and

           A8: i <= k and

           A9: k < j;

          k <= (j -' 1) by A9, NAT_D: 49;

          then (j -' 1) = k or k < (j -' 1) by XXREAL_0: 1;

          then e in B or e in {( LSeg (f,(j -' 1)))} by A7, A8, TARSKI:def 1;

          hence thesis by XBOOLE_0:def 3;

        end;

        let e be object;

        

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

        assume

         A11: e in (B \/ {( LSeg (f,(j -' 1)))});

        per cases by A11, XBOOLE_0:def 3;

          suppose e in B;

          then

          consider k such that

           A12: e = ( LSeg (f,k)) and

           A13: i <= k and

           A14: k < (j -' 1);

          k < j by A10, A14, XXREAL_0: 2;

          hence thesis by A12, A13;

        end;

          suppose

           A15: e in {( LSeg (f,(j -' 1)))};

          1 <= (j -' 1) by A1, A5, XXREAL_0: 2;

          then

           A16: (j -' 1) < j by NAT_D: 51;

          e = ( LSeg (f,(j -' 1))) by A15, TARSKI:def 1;

          hence thesis by A5, A16;

        end;

      end;

      

      thus ( L~ ( mid (f,i,j))) = ( union A) by A1, A2, A3, SPRECT_2: 14

      .= (( union B) \/ ( union {( LSeg (f,(j -' 1)))})) by A6, ZFMISC_1: 78

      .= (( union B) \/ ( LSeg (f,(j -' 1)))) by ZFMISC_1: 25

      .= (( L~ ( mid (f,i,(j -' 1)))) \/ ( LSeg (f,(j -' 1)))) by A1, A5, A4, SPRECT_2: 14;

    end;

    theorem :: SPRECT_3:21

    for f,g be FinSequence of ( TOP-REAL 2) st f is being_S-Seq & g is being_S-Seq & (((f /. ( len f)) `1 ) = ((g /. 1) `1 ) or ((f /. ( len f)) `2 ) = ((g /. 1) `2 )) & ( L~ f) misses ( L~ g) & (( LSeg ((f /. ( len f)),(g /. 1))) /\ ( L~ f)) = {(f /. ( len f))} & (( LSeg ((f /. ( len f)),(g /. 1))) /\ ( L~ g)) = {(g /. 1)} holds (f ^ g) is being_S-Seq

    proof

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

       A1: f is being_S-Seq and

       A2: g is being_S-Seq and

       A3: ((f /. ( len f)) `1 ) = ((g /. 1) `1 ) or ((f /. ( len f)) `2 ) = ((g /. 1) `2 ) and

       A4: ( L~ f) misses ( L~ g) and

       A5: (( LSeg ((f /. ( len f)),(g /. 1))) /\ ( L~ f)) = {(f /. ( len f))} and

       A6: (( LSeg ((f /. ( len f)),(g /. 1))) /\ ( L~ g)) = {(g /. 1)};

      

       A7: ( len g) >= 2 by A2, TOPREAL1:def 8;

      then

       A8: ( len g) >= 1 by XXREAL_0: 2;

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

      then

       A9: (g /. 1) in ( L~ g) by A7, GOBOARD1: 1;

      set h = ( <*(f /. ( len f))*> ^ g);

      

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

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

      then

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

      

      then

       A12: (f . ( len f)) = (f /. ( len f)) by PARTFUN1:def 6

      .= (h . 1) by FINSEQ_1: 41;

      

       A13: ( len h) = (( len <*(f /. ( len f))*>) + ( len g)) by FINSEQ_1: 22

      .= (( len g) + 1) by FINSEQ_1: 39;

      then ( len h) >= (1 + 1) by A8, XREAL_1: 6;

      

      then

       A14: ( mid (h,2,( len h))) = ((h /^ ((1 + 1) -' 1)) | ((( len h) -' 2) + 1)) by FINSEQ_6:def 3

      .= ((h /^ 1) | ((( len h) -' 2) + 1)) by NAT_D: 34

      .= (g | ((( len h) -' 2) + 1)) by FINSEQ_6: 45

      .= (g | (((( len h) -' 1) -' 1) + 1)) by NAT_D: 45

      .= (g | ((( len g) -' 1) + 1)) by A13, NAT_D: 34

      .= (g | ( len g)) by A7, XREAL_1: 235, XXREAL_0: 2

      .= g by FINSEQ_1: 58;

      (f /. ( len f)) in ( L~ f) by A10, A11, GOBOARD1: 1;

      then (f /. ( len f)) <> (g /. 1) by A4, A9, XBOOLE_0: 3;

      then

       A15: h is being_S-Seq by A2, A3, A6, SPRECT_2: 60;

      (( L~ f) /\ ( L~ h)) = (( L~ f) /\ (( LSeg ((f /. ( len f)),(g /. 1))) \/ ( L~ g))) by A2, SPPOL_2: 20

      .= ((( L~ f) /\ ( LSeg ((f /. ( len f)),(g /. 1)))) \/ (( L~ f) /\ ( L~ g))) by XBOOLE_1: 23

      .= ((( L~ f) /\ ( LSeg ((f /. ( len f)),(g /. 1)))) \/ {} ) by A4

      .= {(h . 1)} by A5, A11, A12, PARTFUN1:def 6;

      hence thesis by A1, A12, A15, A14, JORDAN3: 38;

    end;

    theorem :: SPRECT_3:22

    for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) holds (( R_Cut (f,p)) /. 1) = (f /. 1)

    proof

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

      let p be Point of ( TOP-REAL 2);

      set i = ( Index (p,f));

      assume

       A1: p in ( L~ f);

      then

       A2: 1 <= i by JORDAN3: 8;

      i <= ( len f) by A1, JORDAN3: 8;

      then f <> {} by A2;

      then

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

      p = (f . 1) or p <> (f . 1);

      then ( len ( R_Cut (f,p))) = ( Index (p,f)) or ( len ( R_Cut (f,p))) = (( Index (p,f)) + 1) by A1, JORDAN3: 25;

      then 1 <= ( len ( R_Cut (f,p))) by A1, JORDAN3: 8, NAT_1: 11;

      

      hence (( R_Cut (f,p)) /. 1) = (( R_Cut (f,p)) . 1) by FINSEQ_4: 15

      .= (f . 1) by A1, A2, JORDAN3: 24

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

    end;

    theorem :: SPRECT_3:23

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

    proof

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

       A1: 1 <= j and

       A2: j < ( len f) and

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

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

      

       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) in ( LSeg (f,j)) by A1, A5, TOPREAL1: 21;

      then

       A8: ( LSeg ((f /. j),p)) 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 q in ( LSeg (f,i)) & p in ( LSeg (f,j)) & 1 <= i & (i + 1) <= ( len f) & 1 <= j & (j + 1) <= ( len f) holds i <= j & (i = j implies LE (q,p,(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: q in ( LSeg (f,i1)) and

           A14: p 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,i2)) /\ ( LSeg (f,j))) by A3, A14, XBOOLE_0:def 4;

          then

           A18: ( LSeg (f,i2)) meets ( LSeg (f,j));

          then

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

          

           A20: q in (( LSeg (f,i1)) /\ ( LSeg (f,j))) by A4, A8, A13, XBOOLE_0:def 4;

          then

           A21: ( LSeg (f,i1)) meets ( LSeg (f,j));

          then

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

           A23:

          now

            assume

             A24: (i2 + 1) = j;

            (i2 + (1 + 1)) = ((i2 + 1) + 1);

            then (i2 + 2) <= ( len f) by A2, A24, NAT_1: 13;

            then p in {(f /. j)} by A16, A17, A24, TOPREAL1:def 6;

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

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

            hence contradiction by A11, TARSKI:def 1;

          end;

           A25:

          now

            assume that

             A26: (i2 + 1) > j and

             A27: (j + 1) > i2;

            

             A28: j <= i2 by A26, NAT_1: 13;

            i2 <= j by A27, NAT_1: 13;

            hence i2 = j by A28, XXREAL_0: 1;

          end;

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

          then (i2 + 1) = j or i2 = j or (j + 1) = i2 by A25, A19, XXREAL_0: 1;

          then

           A29: i2 >= j by A23, NAT_1: 11;

           A30:

          now

            assume that

             A31: (i1 + 1) > j and

             A32: (j + 1) > i1;

            

             A33: j <= i1 by A31, NAT_1: 13;

            i1 <= j by A32, NAT_1: 13;

            hence i1 = j by A33, XXREAL_0: 1;

          end;

          

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

           A35:

          now

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

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

            hence contradiction;

          end;

           A36:

          now

            

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

            assume i1 = (j + 1);

            then q in {(f /. (j + 1))} by A1, A15, A20, A37, TOPREAL1:def 6;

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

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

          end;

          

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

          then (i1 + 1) = j or i1 = j or (j + 1) = i1 by A30, A22, XXREAL_0: 1;

          then i1 <= j by A36, NAT_1: 11;

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

          assume

           A39: i1 = i2;

           not p in ( LSeg ((f /. j),q)) by A4, A11, Th6;

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

          then LT (q,p,(f /. j),(f /. (j + 1))) by A3, A6, A13, A23, A30, A22, A38, A35, A36, A39, JORDAN3: 28, XXREAL_0: 1;

          hence thesis by A23, A30, A22, A38, A36, A39, JORDAN3:def 6, XXREAL_0: 1;

        end;

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

      end;

    end;

    begin

    theorem :: SPRECT_3:24

    

     Th24: for f be non constant standard special_circular_sequence holds ( LeftComp f) is open & ( RightComp f) is open

    proof

      let f be non constant standard special_circular_sequence;

      ( LeftComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1;

      hence ( LeftComp f) is open by Th8;

      ( RightComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 2;

      hence thesis by Th8;

    end;

    registration

      let f be non constant standard special_circular_sequence;

      cluster ( L~ f) -> non vertical non horizontal;

      coherence

      proof

        ( W-bound ( L~ f)) <> ( E-bound ( L~ f)) by TOPREAL5: 17;

        hence ( L~ f) is non vertical by SPRECT_1: 15;

        ( S-bound ( L~ f)) <> ( N-bound ( L~ f)) by TOPREAL5: 16;

        hence thesis by SPRECT_1: 16;

      end;

      cluster ( LeftComp f) -> being_Region;

      coherence

      proof

        thus ( LeftComp f) is open by Th24;

        ( LeftComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1;

        then

        consider A be Subset of (( TOP-REAL 2) | (( L~ f) ` )) such that

         A1: A = ( LeftComp f) and

         A2: A is a_component by CONNSP_1:def 6;

        A is connected by A2, CONNSP_1:def 5;

        hence thesis by A1, CONNSP_1: 23;

      end;

      cluster ( RightComp f) -> being_Region;

      coherence

      proof

        thus ( RightComp f) is open by Th24;

        ( RightComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 2;

        then

        consider A be Subset of (( TOP-REAL 2) | (( L~ f) ` )) such that

         A3: A = ( RightComp f) and

         A4: A is a_component by CONNSP_1:def 6;

        A is connected by A4, CONNSP_1:def 5;

        hence thesis by A3, CONNSP_1: 23;

      end;

    end

    theorem :: SPRECT_3:25

    

     Th25: for f be non constant standard special_circular_sequence holds ( RightComp f) misses ( L~ f)

    proof

      let f be non constant standard special_circular_sequence;

      (( L~ f) ` ) = (( LeftComp f) \/ ( RightComp f)) by GOBRD12: 10;

      then ( RightComp f) c= (( L~ f) ` ) by XBOOLE_1: 7;

      hence thesis by SUBSET_1: 23;

    end;

    theorem :: SPRECT_3:26

    

     Th26: for f be non constant standard special_circular_sequence holds ( LeftComp f) misses ( L~ f)

    proof

      let f be non constant standard special_circular_sequence;

      (( L~ f) ` ) = (( LeftComp f) \/ ( RightComp f)) by GOBRD12: 10;

      then ( LeftComp f) c= (( L~ f) ` ) by XBOOLE_1: 7;

      hence thesis by SUBSET_1: 23;

    end;

    theorem :: SPRECT_3:27

    

     Th27: for f be non constant standard special_circular_sequence holds ( i_w_n f) < ( i_e_n f)

    proof

      let f be non constant standard special_circular_sequence;

      set G = ( GoB f);

      

       A1: ( i_w_n f) <= ( len G) by JORDAN5D: 45;

      

       A2: (G * (( i_w_n f),( width G))) = ( N-min ( L~ f)) by JORDAN5D:def 7;

      assume

       A3: ( i_w_n f) >= ( i_e_n f);

      

       A4: 1 <= ( i_e_n f) by JORDAN5D: 45;

      

       A5: (( N-min ( L~ f)) `1 ) < (( N-max ( L~ f)) `1 ) by SPRECT_2: 51;

      

       A6: (G * (( i_e_n f),( width G))) = ( N-max ( L~ f)) by JORDAN5D:def 8;

      then ( i_w_n f) <> ( i_e_n f) by A5, JORDAN5D:def 7;

      then

       A7: ( i_w_n f) > ( i_e_n f) by A3, XXREAL_0: 1;

      ( width G) > 1 by GOBOARD7: 33;

      hence contradiction by A1, A2, A4, A6, A5, A7, GOBOARD5: 3;

    end;

    theorem :: SPRECT_3:28

    

     Th28: for f be non constant standard special_circular_sequence holds ex i st 1 <= i & i < ( len ( GoB f)) & ( N-min ( L~ f)) = (( GoB f) * (i,( width ( GoB f))))

    proof

      let f be non constant standard special_circular_sequence;

      take i = ( i_w_n f);

      thus 1 <= i by JORDAN5D: 45;

      ( i_e_n f) <= ( len ( GoB f)) by JORDAN5D: 45;

      hence i < ( len ( GoB f)) by Th27, XXREAL_0: 2;

      thus thesis by JORDAN5D:def 7;

    end;

    theorem :: SPRECT_3:29

    

     Th29: for f be clockwise_oriented non constant standard special_circular_sequence st i in ( dom ( GoB f)) & (f /. 1) = (( GoB f) * (i,( width ( GoB f)))) & (f /. 1) = ( N-min ( L~ f)) holds (f /. 2) = (( GoB f) * ((i + 1),( width ( GoB f)))) & (f /. (( len f) -' 1)) = (( GoB f) * (i,(( width ( GoB f)) -' 1)))

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence such that

       A1: i in ( dom ( GoB f)) and

       A2: (f /. 1) = (( GoB f) * (i,( width ( GoB f)))) and

       A3: (f /. 1) = ( N-min ( L~ f));

      

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

      4 < ( len f) by GOBOARD7: 34;

      then

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

      

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

      

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

      then

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

      

       A9: 1 <= ( width ( GoB f)) by GOBRD11: 34;

      

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

      

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

      then

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

      then

      consider i1,j1 be Nat such that

       A13: [i1, j1] in ( Indices ( GoB f)) and

       A14: (f /. 2) = (( GoB f) * (i1,j1)) by GOBOARD2: 14;

      

       A15: 1 <= j1 by A13, MATRIX_0: 32;

      

       A16: j1 <= ( width ( GoB f)) by A13, MATRIX_0: 32;

      

       A17: 1 <= i1 by A13, MATRIX_0: 32;

      

       A18: i1 <= ( len ( GoB f)) by A13, MATRIX_0: 32;

      now

        

         A19: ((f /. 2) `2 ) = (( N-min ( L~ f)) `2 ) by A10, PSCOMP_1: 39

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

        assume

         A20: j1 < ( width ( GoB f));

        ((( GoB f) * (i1,( width ( GoB f)))) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A9, A17, A18, GOBOARD5: 1

        .= ( N-bound ( L~ f)) by JORDAN5D: 40;

        hence contradiction by A14, A15, A17, A18, A20, A19, GOBOARD5: 4;

      end;

      then

       A21: j1 = ( width ( GoB f)) by A16, XXREAL_0: 1;

       A22:

      now

        assume i > i1;

        then ((f /. 2) `1 ) < (( N-min ( L~ f)) `1 ) by A2, A3, A14, A4, A15, A17, A21, GOBOARD5: 3;

        hence contradiction by A10, PSCOMP_1: 39;

      end;

      

       A23: 1 <= i by A1, FINSEQ_3: 25;

      then

       A24: [i, ( width ( GoB f))] in ( Indices ( GoB f)) by A9, A4, MATRIX_0: 30;

      ( |.(i - i1).| + 0 ) = ( |.(i - i1).| + |.(( width ( GoB f)) - ( width ( GoB f))).|) by ABSVALUE: 2

      .= 1 by A2, A12, A13, A14, A8, A24, A21, GOBOARD5: 12;

      hence

       A25: (f /. 2) = (( GoB f) * ((i + 1),( width ( GoB f)))) by A14, A21, A22, SEQM_3: 41;

      

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

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

      then

       A27: (( len f) -' 1) in ( dom f) by A26, FINSEQ_3: 25;

      then

      consider i2,j2 be Nat such that

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

       A29: (f /. (( len f) -' 1)) = (( GoB f) * (i2,j2)) by GOBOARD2: 14;

      

       A30: 1 <= i2 by A28, MATRIX_0: 32;

      

       A31: j2 <= ( width ( GoB f)) by A28, MATRIX_0: 32;

      

       A32: i2 <= ( len ( GoB f)) by A28, MATRIX_0: 32;

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

      then

       A33: ( |.(i2 - i).| + |.(j2 - ( width ( GoB f))).|) = 1 by A2, A24, A6, A5, A27, A28, A29, GOBOARD5: 12;

      per cases by A33, SEQM_3: 42;

        suppose that

         A34: |.(i2 - i).| = 1 and

         A35: j2 = ( width ( GoB f));

        ((f /. (( len f) -' 1)) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A9, A29, A30, A32, A35, GOBOARD5: 1

        .= (( N-min ( L~ f)) `2 ) by A2, A3, A9, A23, A4, GOBOARD5: 1

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

        then

         A36: (f /. (( len f) -' 1)) in ( N-most ( L~ f)) by A11, A27, GOBOARD1: 1, SPRECT_2: 10;

        now

          per cases by A34, SEQM_3: 41;

            suppose i > i2;

            then ((f /. (( len f) -' 1)) `1 ) < (( N-min ( L~ f)) `1 ) by A2, A3, A9, A4, A29, A30, A35, GOBOARD5: 3;

            hence contradiction by A36, PSCOMP_1: 39;

          end;

            suppose (i + 1) = i2;

            then 2 >= (( len f) -' 1) by A25, A26, A29, A35, GOBOARD7: 37;

            then (2 + 1) >= ( len f) by NAT_D: 52;

            hence contradiction by GOBOARD7: 34, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

        suppose that

         A37: |.(j2 - ( width ( GoB f))).| = 1 and

         A38: i2 = i;

        ( width ( GoB f)) = (j2 + 1) by A31, A37, SEQM_3: 41;

        hence thesis by A29, A38, NAT_D: 34;

      end;

    end;

    theorem :: SPRECT_3:30

    for f be non constant standard special_circular_sequence st 1 <= i & i < j & j <= ( len f) & (f /. 1) in ( L~ ( mid (f,i,j))) holds i = 1 or j = ( len f)

    proof

      let f be non constant standard special_circular_sequence such that

       A1: 1 <= i and

       A2: i < j and

       A3: j <= ( len f);

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

      then

       A4: (f /. 1) in ( LSeg (f,1)) by TOPREAL1: 21;

      assume (f /. 1) in ( L~ ( mid (f,i,j)));

      then

      consider n such that

       A5: 1 <= n and

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

       A7: (f /. 1) in ( LSeg (( mid (f,i,j)),n)) by SPPOL_2: 13;

      n < ( len ( mid (f,i,j))) by A6, NAT_1: 13;

      then

       A8: n < ((j -' i) + 1) by A1, A2, A3, JORDAN4: 8;

      then ( LSeg (( mid (f,i,j)),n)) = ( LSeg (f,((n + i) -' 1))) by A1, A2, A3, A5, JORDAN4: 19;

      then

       A9: (f /. 1) in (( LSeg (f,1)) /\ ( LSeg (f,((n + i) -' 1)))) by A7, A4, XBOOLE_0:def 4;

      then

       A10: ( LSeg (f,1)) meets ( LSeg (f,((n + i) -' 1)));

      assume that

       A11: i <> 1 and

       A12: j <> ( len f);

      per cases by A10, GOBOARD5:def 4;

        suppose (1 + 1) >= ((n + i) -' 1);

        then

         A13: (n + i) <= (2 + 1) by NAT_D: 52;

        i > 1 by A1, A11, XXREAL_0: 1;

        then

         A14: i >= (1 + 1) by NAT_1: 13;

        (n + i) >= (i + 1) by A5, XREAL_1: 6;

        then (i + 1) <= (2 + 1) by A13, XXREAL_0: 2;

        then i <= 2 by XREAL_1: 6;

        then

         A15: i = 2 by A14, XXREAL_0: 1;

        then n <= 1 by A13, XREAL_1: 6;

        then n = 1 by A5, XXREAL_0: 1;

        then

         A16: ((n + i) -' 1) = 2 by A15, NAT_D: 34;

        

         A17: 2 < ( len f) by GOBOARD7: 34, XXREAL_0: 2;

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

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

        then (f /. 1) = (f /. 2) by A9, A16, TARSKI:def 1;

        hence contradiction by A17, GOBOARD7: 36;

      end;

        suppose

         A18: (((n + i) -' 1) + 1) >= ( len f);

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

        then

         A19: ( len f) <= (n + i) by A5, A18, XREAL_1: 235, XXREAL_0: 2;

        (((j -' i) + 1) + i) = (((j -' i) + i) + 1)

        .= (j + 1) by A2, XREAL_1: 235;

        then (n + i) < (j + 1) by A8, XREAL_1: 6;

        then

         A20: (n + i) <= j by NAT_1: 13;

        j < ( len f) by A3, A12, XXREAL_0: 1;

        hence contradiction by A19, A20, XXREAL_0: 2;

      end;

    end;

    theorem :: SPRECT_3:31

    for f be clockwise_oriented non constant standard special_circular_sequence st (f /. 1) = ( N-min ( L~ f)) holds ( LSeg ((f /. 1),(f /. 2))) c= ( L~ ( SpStSeq ( L~ f)))

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence;

      

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

      assume

       A2: (f /. 1) = ( N-min ( L~ f));

      then

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

      

       A4: ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) c= ( L~ ( SpStSeq ( L~ f))) by Th14;

      (f /. 1) in ( LSeg (( NW-corner ( L~ f)),( NE-corner ( L~ f)))) by A2, Th15;

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

      hence thesis by A4;

    end;

    begin

    theorem :: SPRECT_3:32

    

     Th32: for f be rectangular FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st p in ( L~ f) holds (p `1 ) = ( W-bound ( L~ f)) or (p `1 ) = ( E-bound ( L~ f)) or (p `2 ) = ( S-bound ( L~ f)) or (p `2 ) = ( N-bound ( L~ f))

    proof

      let f be rectangular FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) such that

       A1: p in ( L~ f);

      consider D be non vertical non horizontal non empty compact Subset of ( TOP-REAL 2) such that

       A2: f = ( SpStSeq D) by SPRECT_1:def 2;

      ( L~ f) = ((( LSeg (( NW-corner D),( NE-corner D))) \/ ( LSeg (( NE-corner D),( SE-corner D)))) \/ (( LSeg (( SE-corner D),( SW-corner D))) \/ ( LSeg (( SW-corner D),( NW-corner D))))) by A2, SPRECT_1: 41;

      then

       A3: p in (( LSeg (( NW-corner D),( NE-corner D))) \/ ( LSeg (( NE-corner D),( SE-corner D)))) or p in (( LSeg (( SE-corner D),( SW-corner D))) \/ ( LSeg (( SW-corner D),( NW-corner D)))) by A1, XBOOLE_0:def 3;

      per cases by A3, XBOOLE_0:def 3;

        suppose

         A4: p in ( LSeg (( NW-corner D),( NE-corner D)));

        

         A5: ( N-bound ( L~ ( SpStSeq D))) = ( N-bound D) by SPRECT_1: 60;

        then

         A6: (( NE-corner D) `2 ) = ( N-bound ( L~ f)) by A2, EUCLID: 52;

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

        hence thesis by A4, A6, GOBOARD7: 6;

      end;

        suppose

         A7: p in ( LSeg (( NE-corner D),( SE-corner D)));

        

         A8: ( E-bound ( L~ ( SpStSeq D))) = ( E-bound D) by SPRECT_1: 61;

        then

         A9: (( SE-corner D) `1 ) = ( E-bound ( L~ f)) by A2, EUCLID: 52;

        (( NE-corner D) `1 ) = ( E-bound ( L~ f)) by A2, A8, EUCLID: 52;

        hence thesis by A7, A9, GOBOARD7: 5;

      end;

        suppose

         A10: p in ( LSeg (( SE-corner D),( SW-corner D)));

        

         A11: ( S-bound ( L~ ( SpStSeq D))) = ( S-bound D) by SPRECT_1: 59;

        then

         A12: (( SW-corner D) `2 ) = ( S-bound ( L~ f)) by A2, EUCLID: 52;

        (( SE-corner D) `2 ) = ( S-bound ( L~ f)) by A2, A11, EUCLID: 52;

        hence thesis by A10, A12, GOBOARD7: 6;

      end;

        suppose

         A13: p in ( LSeg (( SW-corner D),( NW-corner D)));

        

         A14: ( W-bound ( L~ ( SpStSeq D))) = ( W-bound D) by SPRECT_1: 58;

        then

         A15: (( NW-corner D) `1 ) = ( W-bound ( L~ f)) by A2, EUCLID: 52;

        (( SW-corner D) `1 ) = ( W-bound ( L~ f)) by A2, A14, EUCLID: 52;

        hence thesis by A13, A15, GOBOARD7: 5;

      end;

    end;

    registration

      cluster rectangular for special_circular_sequence;

      existence

      proof

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

        ( SpStSeq C) is special_circular_sequence;

        hence thesis;

      end;

    end

    theorem :: SPRECT_3:33

    

     Th33: for f be rectangular special_circular_sequence, g be S-Sequence_in_R2 st (g /. 1) in ( LeftComp f) & (g /. ( len g)) in ( RightComp f) holds ( L~ f) meets ( L~ g)

    proof

      let f be rectangular special_circular_sequence, g be S-Sequence_in_R2 such that

       A1: (g /. 1) in ( LeftComp f) and

       A2: (g /. ( len g)) in ( RightComp f);

      

       A3: ( len g) >= 2 by TOPREAL1:def 8;

      then (g /. 1) in ( L~ g) by JORDAN3: 1;

      then (g /. 1) in (( LeftComp f) /\ ( L~ g)) by A1, XBOOLE_0:def 4;

      then

       A4: ( LeftComp f) meets ( L~ g);

      (g /. ( len g)) in ( L~ g) by A3, JORDAN3: 1;

      then (g /. ( len g)) in (( RightComp f) /\ ( L~ g)) by A2, XBOOLE_0:def 4;

      then

       A5: ( RightComp f) meets ( L~ g);

      

       A6: ( LeftComp f) misses ( RightComp f) by SPRECT_1: 88;

      assume ( L~ f) misses ( L~ g);

      then ( L~ g) c= (( L~ f) ` ) by SUBSET_1: 23;

      then

       A7: ( L~ g) c= (( LeftComp f) \/ ( RightComp f)) by GOBRD12: 10;

      

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

      

       A9: ( RightComp f) is open by Th24;

      ( LeftComp f) is open by Th24;

      hence contradiction by A7, A9, A4, A5, A6, A8, JORDAN6: 10, TOPREAL5: 1;

    end;

    theorem :: SPRECT_3:34

    

     Th34: for f be rectangular special_circular_sequence holds ( SpStSeq ( L~ f)) = f

    proof

      let f be rectangular special_circular_sequence;

      set C = ( L~ f), g = ( SpStSeq C);

      consider D be non vertical non horizontal non empty compact Subset of ( TOP-REAL 2) such that

       A1: f = ( SpStSeq D) by SPRECT_1:def 2;

      

       A2: 5 = ( len f) by SPRECT_1: 82;

      ( SpStSeq ( L~ f)) = ( <*( NW-corner ( L~ f)), ( NE-corner ( L~ f)), ( SE-corner ( L~ f))*> ^ <*( SW-corner ( L~ f)), ( NW-corner ( L~ f))*>) by SPRECT_1:def 1;

      

      then

       A3: ( len g) = (( len <*( NW-corner ( L~ f)), ( NE-corner ( L~ f)), ( SE-corner ( L~ f))*>) + ( len <*( SW-corner ( L~ f)), ( NW-corner ( L~ f))*>)) by FINSEQ_1: 22

      .= (3 + ( len <*( SW-corner ( L~ f)), ( NW-corner ( L~ f))*>)) by FINSEQ_1: 45

      .= (3 + 2) by FINSEQ_1: 44;

      

       A4: for i be Nat st i in ( dom f) holds (f /. i) = (g /. i)

      proof

        let i be Nat;

        assume

         A5: i in ( dom f);

        then

         A6: 0 <> i by FINSEQ_3: 25;

        

         A7: i <= ( len f) by A5, FINSEQ_3: 25;

        

         A8: (f /. 1) = ( W-max C) by SPRECT_1: 83

        .= ( NW-corner D) by A1, SPRECT_1: 75

        .= ( NW-corner C) by A1, SPRECT_1: 62

        .= (g /. 1) by SPRECT_1: 35;

        i <= 5 by A2, A7;

        then i = 0 or ... or i = 5;

        per cases by A6;

          suppose i = 1;

          hence thesis by A8;

        end;

          suppose

           A9: i = 2;

          

          hence (f /. i) = ( E-max C) by SPRECT_1: 84

          .= ( NE-corner D) by A1, SPRECT_1: 79

          .= ( NE-corner C) by A1, SPRECT_1: 63

          .= (g /. i) by A9, SPRECT_1: 36;

        end;

          suppose

           A10: i = 3;

          

          hence (f /. i) = ( E-min C) by SPRECT_1: 85

          .= ( SE-corner D) by A1, SPRECT_1: 78

          .= ( SE-corner C) by A1, SPRECT_1: 65

          .= (g /. i) by A10, SPRECT_1: 37;

        end;

          suppose

           A11: i = 4;

          

          hence (f /. i) = ( W-min C) by SPRECT_1: 86

          .= ( SW-corner D) by A1, SPRECT_1: 74

          .= ( SW-corner C) by A1, SPRECT_1: 64

          .= (g /. i) by A11, SPRECT_1: 38;

        end;

          suppose

           A12: i = 5;

          

          hence (f /. i) = (f /. 1) by A2, FINSEQ_6:def 1

          .= (g /. i) by A3, A8, A12, FINSEQ_6:def 1;

        end;

      end;

      ( dom f) = ( dom g) by A2, A3, FINSEQ_3: 29;

      hence thesis by A4, FINSEQ_5: 12;

    end;

    theorem :: SPRECT_3:35

    

     Th35: for f be rectangular special_circular_sequence holds ( L~ f) = { p where p be Point of ( TOP-REAL 2) : (p `1 ) = ( W-bound ( L~ f)) & (p `2 ) <= ( N-bound ( L~ f)) & (p `2 ) >= ( S-bound ( L~ f)) or (p `1 ) <= ( E-bound ( L~ f)) & (p `1 ) >= ( W-bound ( L~ f)) & (p `2 ) = ( N-bound ( L~ f)) or (p `1 ) <= ( E-bound ( L~ f)) & (p `1 ) >= ( W-bound ( L~ f)) & (p `2 ) = ( S-bound ( L~ f)) or (p `1 ) = ( E-bound ( L~ f)) & (p `2 ) <= ( N-bound ( L~ f)) & (p `2 ) >= ( S-bound ( L~ f)) }

    proof

      let f be rectangular special_circular_sequence;

      set C = ( L~ f), E = { p : (p `1 ) = ( E-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) }, S = { p : (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( S-bound C) }, N = { p : (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( N-bound C) }, W = { p : (p `1 ) = ( W-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) };

      

       A1: ( LSeg (( SE-corner C),( NE-corner C))) = E by SPRECT_1: 23;

      

       A2: ( LSeg (( SW-corner C),( SE-corner C))) = S by SPRECT_1: 24;

      

       A3: ( LSeg (( SW-corner C),( NW-corner C))) = W by SPRECT_1: 26;

      

       A4: ( LSeg (( NW-corner C),( NE-corner C))) = N by SPRECT_1: 25;

      

       A5: C = ( L~ ( SpStSeq C)) by Th34;

      thus C c= { p where p be Point of ( TOP-REAL 2) : (p `1 ) = ( W-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) or (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( N-bound C) or (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( S-bound C) or (p `1 ) = ( E-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) }

      proof

        let x be object;

        assume

         A6: x in C;

        then

        reconsider q = x as Point of ( TOP-REAL 2);

        q in ((( LSeg (( NW-corner C),( NE-corner C))) \/ ( LSeg (( NE-corner C),( SE-corner C)))) \/ (( LSeg (( SE-corner C),( SW-corner C))) \/ ( LSeg (( SW-corner C),( NW-corner C))))) by A5, A6, SPRECT_1: 41;

        then q in (( LSeg (( NW-corner C),( NE-corner C))) \/ ( LSeg (( NE-corner C),( SE-corner C)))) or q in (( LSeg (( SE-corner C),( SW-corner C))) \/ ( LSeg (( SW-corner C),( NW-corner C)))) by XBOOLE_0:def 3;

        then q in ( LSeg (( NW-corner C),( NE-corner C))) or q in ( LSeg (( NE-corner C),( SE-corner C))) or q in ( LSeg (( SE-corner C),( SW-corner C))) or q in ( LSeg (( SW-corner C),( NW-corner C))) by XBOOLE_0:def 3;

        then (ex p st x = p & (p `1 ) = ( E-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C)) or (ex p st x = p & (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( S-bound C)) or (ex p st x = p & (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( N-bound C)) or ex p st x = p & (p `1 ) = ( W-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) by A1, A2, A4, A3;

        hence thesis;

      end;

      let x be object;

      assume x in { p where p be Point of ( TOP-REAL 2) : (p `1 ) = ( W-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) or (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( N-bound C) or (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( S-bound C) or (p `1 ) = ( E-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) };

      then ex p st x = p & ((p `1 ) = ( W-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C) or (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( N-bound C) or (p `1 ) <= ( E-bound C) & (p `1 ) >= ( W-bound C) & (p `2 ) = ( S-bound C) or (p `1 ) = ( E-bound C) & (p `2 ) <= ( N-bound C) & (p `2 ) >= ( S-bound C));

      then x in ( LSeg (( NW-corner C),( NE-corner C))) or x in ( LSeg (( NE-corner C),( SE-corner C))) or x in ( LSeg (( SE-corner C),( SW-corner C))) or x in ( LSeg (( SW-corner C),( NW-corner C))) by A1, A2, A4, A3;

      then x in (( LSeg (( NW-corner C),( NE-corner C))) \/ ( LSeg (( NE-corner C),( SE-corner C)))) or x in (( LSeg (( SE-corner C),( SW-corner C))) \/ ( LSeg (( SW-corner C),( NW-corner C)))) by XBOOLE_0:def 3;

      then x in ((( LSeg (( NW-corner C),( NE-corner C))) \/ ( LSeg (( NE-corner C),( SE-corner C)))) \/ (( LSeg (( SE-corner C),( SW-corner C))) \/ ( LSeg (( SW-corner C),( NW-corner C))))) by XBOOLE_0:def 3;

      hence thesis by A5, SPRECT_1: 41;

    end;

    theorem :: SPRECT_3:36

    

     Th36: for f be rectangular special_circular_sequence holds ( GoB f) = (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)))

    proof

      let f be rectangular special_circular_sequence;

      set G = (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))), v1 = ( Incr ( X_axis f)), v2 = ( Incr ( Y_axis f));

      

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

      

       A2: (f /. 1) = ( N-min ( L~ f)) by SPRECT_1: 83;

      then

       A3: ((f /. 1) `1 ) < ((f /. 2) `1 ) by A1, SPRECT_2: 51;

      

       A4: ((f /. 2) `2 ) = ((f /. 1) `2 ) by A2, A1, PSCOMP_1: 37;

      

       A5: (f /. 4) = ( S-min ( L~ f)) by SPRECT_1: 86;

      

       A6: (f /. 3) = ( S-max ( L~ f)) by SPRECT_1: 85;

      then

       A7: ((f /. 3) `2 ) = ((f /. 4) `2 ) by A5, PSCOMP_1: 53;

      

       A8: ( len <*((f /. 3) `1 ), ((f /. 4) `1 ), ((f /. 5) `1 )*>) = 3 by FINSEQ_1: 45;

      

       A9: ( len f) = 5 by SPRECT_1: 82;

      then

       A10: (f /. 1) = (f /. 5) by FINSEQ_6:def 1;

      set g = <*((f /. 1) `1 ), ((f /. 2) `1 )*>;

      reconsider h = ( <*((f /. 1) `1 ), ((f /. 2) `1 )*> ^ <*((f /. 3) `1 ), ((f /. 4) `1 ), ((f /. 5) `1 )*>) as FinSequence of REAL by RVSUM_1: 145;

      

       A11: (f /. 3) = ( E-min ( L~ f)) by SPRECT_1: 85;

      

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

      then

       A13: ((f /. 3) `1 ) = ((f /. 2) `1 ) by A11, PSCOMP_1: 45;

      

       A14: ( len g) = 2 by FINSEQ_1: 44;

      

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

      

       A16: g is increasing

      proof

        

         A17: (g . 2) = ((f /. 2) `1 ) by FINSEQ_1: 44;

        

         A18: (g . 1) = ((f /. 1) `1 ) by FINSEQ_1: 44;

        let n, m such that

         A19: n in ( dom g) and

         A20: m in ( dom g) and

         A21: n < m;

        

         A22: m = 1 or m = 2 by A15, A20, TARSKI:def 2;

        n = 1 or n = 2 by A15, A19, TARSKI:def 2;

        hence (g . n) < (g . m) by A2, A1, A21, A18, A17, A22, SPRECT_2: 51;

      end;

      

       A23: (f /. 4) = ( W-min ( L~ f)) by SPRECT_1: 86;

      

       A24: ( len h) = (( len <*((f /. 1) `1 ), ((f /. 2) `1 )*>) + ( len <*((f /. 3) `1 ), ((f /. 4) `1 ), ((f /. 5) `1 )*>)) by FINSEQ_1: 22

      .= (( len <*((f /. 1) `1 ), ((f /. 2) `1 )*>) + 3) by FINSEQ_1: 45

      .= (2 + 3) by FINSEQ_1: 44

      .= ( len f) by SPRECT_1: 82;

      for n st n in ( dom h) holds (h . n) = ((f /. n) `1 )

      proof

        let n;

        assume

         A25: n in ( dom h);

        then

         A26: 1 <= n by FINSEQ_3: 25;

        n <= 5 by A9, A24, A25, FINSEQ_3: 25;

        then n = 0 or ... or n = 5;

        per cases by A26;

          suppose

           A27: n = 1;

          then n in ( dom g) by A14, FINSEQ_3: 25;

          

          hence (h . n) = ( <*((f /. 1) `1 ), ((f /. 2) `1 )*> . 1) by A27, FINSEQ_1:def 7

          .= ((f /. n) `1 ) by A27, FINSEQ_1: 44;

        end;

          suppose

           A28: n = 2;

          then n in ( dom g) by A14, FINSEQ_3: 25;

          

          hence (h . n) = ( <*((f /. 1) `1 ), ((f /. 2) `1 )*> . 2) by A28, FINSEQ_1:def 7

          .= ((f /. n) `1 ) by A28, FINSEQ_1: 44;

        end;

          suppose

           A29: n = 3;

          

          hence (h . n) = (h . (2 + 1))

          .= ( <*((f /. 3) `1 ), ((f /. 4) `1 ), ((f /. 5) `1 )*> . 1) by A14, A8, FINSEQ_1: 65

          .= ((f /. n) `1 ) by A29, FINSEQ_1: 45;

        end;

          suppose

           A30: n = 4;

          

          hence (h . n) = (h . (2 + 2))

          .= ( <*((f /. 3) `1 ), ((f /. 4) `1 ), ((f /. 5) `1 )*> . 2) by A14, A8, FINSEQ_1: 65

          .= ((f /. n) `1 ) by A30, FINSEQ_1: 45;

        end;

          suppose

           A31: n = 5;

          

          hence (h . n) = (h . (2 + 3))

          .= ( <*((f /. 3) `1 ), ((f /. 4) `1 ), ((f /. 5) `1 )*> . 3) by A14, A8, FINSEQ_1: 65

          .= ((f /. n) `1 ) by A31, FINSEQ_1: 45;

        end;

      end;

      then

       A32: ( X_axis f) = h by A24, GOBOARD1:def 1;

      

       A33: ( rng g) = {((f /. 1) `1 ), ((f /. 2) `1 )} by FINSEQ_2: 127;

      

       A34: (f /. 1) = ( W-max ( L~ f)) by SPRECT_1: 83;

      then

       A35: ((f /. 4) `2 ) < ((f /. 5) `2 ) by A23, A10, SPRECT_2: 57;

      reconsider vv1 = <*((f /. 1) `1 ), ((f /. 2) `1 )*> as FinSequence of REAL by RVSUM_1: 145;

       {((f /. 3) `1 ), ((f /. 4) `1 ), ((f /. 5) `1 )} c= {((f /. 1) `1 ), ((f /. 2) `1 )}

      proof

        let x be object;

        assume

         A36: x in {((f /. 3) `1 ), ((f /. 4) `1 ), ((f /. 5) `1 )};

        per cases by A36, ENUMSET1:def 1;

          suppose x = ((f /. 3) `1 );

          then x = ((f /. 2) `1 ) by A12, A11, PSCOMP_1: 45;

          hence thesis by TARSKI:def 2;

        end;

          suppose x = ((f /. 4) `1 );

          then x = ((f /. 1) `1 ) by A34, A23, PSCOMP_1: 29;

          hence thesis by TARSKI:def 2;

        end;

          suppose x = ((f /. 5) `1 );

          then x = ((f /. 1) `1 ) by A9, FINSEQ_6:def 1;

          hence thesis by TARSKI:def 2;

        end;

      end;

      

      then

       A37: ( rng g) = (( rng <*((f /. 1) `1 ), ((f /. 2) `1 )*>) \/ {((f /. 3) `1 ), ((f /. 4) `1 ), ((f /. 5) `1 )}) by A33, XBOOLE_1: 12

      .= (( rng <*((f /. 1) `1 ), ((f /. 2) `1 )*>) \/ ( rng <*((f /. 3) `1 ), ((f /. 4) `1 ), ((f /. 5) `1 )*>)) by FINSEQ_2: 128

      .= ( rng ( X_axis f)) by A32, FINSEQ_1: 31;

      ( len g) = 2 by FINSEQ_1: 44

      .= ( card ( rng ( X_axis f))) by A33, A37, A3, CARD_2: 57;

      then

       A38: v1 = vv1 by A37, A16, SEQ_4:def 21;

      then

       A39: (v1 . 1) = ((f /. 1) `1 ) by FINSEQ_1: 44;

      set g = <*((f /. 4) `2 ), ((f /. 5) `2 )*>;

      reconsider h = ( <*((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )*> ^ <*((f /. 4) `2 ), ((f /. 5) `2 )*>) as FinSequence of REAL by RVSUM_1: 145;

      

       A40: ( len h) = (( len <*((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )*>) + ( len <*((f /. 4) `2 ), ((f /. 5) `2 )*>)) by FINSEQ_1: 22

      .= (( len <*((f /. 4) `2 ), ((f /. 5) `2 )*>) + 3) by FINSEQ_1: 45

      .= (2 + 3) by FINSEQ_1: 44

      .= ( len f) by SPRECT_1: 82;

      

       A41: ( len <*((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )*>) = 3 by FINSEQ_1: 45;

      

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

      

       A43: g is increasing

      proof

        

         A44: (g . 2) = ((f /. 5) `2 ) by FINSEQ_1: 44;

        

         A45: (g . 1) = ((f /. 4) `2 ) by FINSEQ_1: 44;

        let n, m such that

         A46: n in ( dom g) and

         A47: m in ( dom g) and

         A48: n < m;

        

         A49: m = 1 or m = 2 by A42, A47, TARSKI:def 2;

        n = 1 or n = 2 by A42, A46, TARSKI:def 2;

        hence (g . n) < (g . m) by A34, A23, A10, A48, A45, A44, A49, SPRECT_2: 57;

      end;

      

       A50: (v1 . 2) = ((f /. 2) `1 ) by A38, FINSEQ_1: 44;

      

       A51: ( len g) = 2 by FINSEQ_1: 44;

      for n st n in ( dom h) holds (h . n) = ((f /. n) `2 )

      proof

        let n;

        assume

         A52: n in ( dom h);

        then

         A53: 1 <= n by FINSEQ_3: 25;

        n <= 5 by A9, A40, A52, FINSEQ_3: 25;

        then n = 0 or ... or n = 5;

        per cases by A53;

          suppose

           A54: n = 1;

          then n in ( dom <*((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )*>) by A41, FINSEQ_3: 25;

          

          hence (h . n) = ( <*((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )*> . 1) by A54, FINSEQ_1:def 7

          .= ((f /. n) `2 ) by A54, FINSEQ_1: 45;

        end;

          suppose

           A55: n = 2;

          then n in ( dom <*((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )*>) by A41, FINSEQ_3: 25;

          

          hence (h . n) = ( <*((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )*> . 2) by A55, FINSEQ_1:def 7

          .= ((f /. n) `2 ) by A55, FINSEQ_1: 45;

        end;

          suppose

           A56: n = 3;

          then n in ( dom <*((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )*>) by A41, FINSEQ_3: 25;

          

          hence (h . n) = ( <*((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )*> . 3) by A56, FINSEQ_1:def 7

          .= ((f /. n) `2 ) by A56, FINSEQ_1: 45;

        end;

          suppose

           A57: n = 4;

          

          hence (h . n) = (h . (3 + 1))

          .= ( <*((f /. 4) `2 ), ((f /. 5) `2 )*> . 1) by A51, A41, FINSEQ_1: 65

          .= ((f /. n) `2 ) by A57, FINSEQ_1: 44;

        end;

          suppose

           A58: n = 5;

          

          hence (h . n) = (h . (2 + 3))

          .= ( <*((f /. 4) `2 ), ((f /. 5) `2 )*> . 2) by A51, A41, FINSEQ_1: 65

          .= ((f /. n) `2 ) by A58, FINSEQ_1: 44;

        end;

      end;

      then

       A59: ( Y_axis f) = h by A40, GOBOARD1:def 2;

      

       A60: ( rng g) = {((f /. 4) `2 ), ((f /. 5) `2 )} by FINSEQ_2: 127;

       {((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )} c= {((f /. 4) `2 ), ((f /. 5) `2 )}

      proof

        let x be object;

        assume

         A61: x in {((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )};

        per cases by A61, ENUMSET1:def 1;

          suppose x = ((f /. 1) `2 );

          hence thesis by A10, TARSKI:def 2;

        end;

          suppose x = ((f /. 2) `2 );

          then x = ((f /. 1) `2 ) by A2, A1, PSCOMP_1: 37;

          hence thesis by A10, TARSKI:def 2;

        end;

          suppose x = ((f /. 3) `2 );

          then x = ((f /. 4) `2 ) by A6, A5, PSCOMP_1: 53;

          hence thesis by TARSKI:def 2;

        end;

      end;

      

      then

       A62: ( rng g) = ( {((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )} \/ {((f /. 4) `2 ), ((f /. 5) `2 )}) by A60, XBOOLE_1: 12

      .= (( rng <*((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )*>) \/ {((f /. 4) `2 ), ((f /. 5) `2 )}) by FINSEQ_2: 128

      .= (( rng <*((f /. 1) `2 ), ((f /. 2) `2 ), ((f /. 3) `2 )*>) \/ ( rng <*((f /. 4) `2 ), ((f /. 5) `2 )*>)) by FINSEQ_2: 127

      .= ( rng ( Y_axis f)) by A59, FINSEQ_1: 31;

      reconsider vv2 = <*((f /. 4) `2 ), ((f /. 1) `2 )*> as FinSequence of REAL by RVSUM_1: 145;

      ( len g) = 2 by FINSEQ_1: 44

      .= ( card ( rng ( Y_axis f))) by A60, A62, A35, CARD_2: 57;

      then

       A63: v2 = vv2 by A10, A62, A43, SEQ_4:def 21;

      then

       A64: (v2 . 1) = ((f /. 4) `2 ) by FINSEQ_1: 44;

      

       A65: (v2 . 2) = ((f /. 1) `2 ) by A63, FINSEQ_1: 44;

      

       A66: ((f /. 1) `1 ) = ((f /. 4) `1 ) by A34, A23, PSCOMP_1: 29;

      

       A67: for n, m st [n, m] in ( Indices G) holds (G * (n,m)) = |[(v1 . n), (v2 . m)]|

      proof

        let n, m;

        assume [n, m] in ( Indices G);

        then

         A68: [n, m] in { [1, 1], [1, 2], [2, 1], [2, 2]} by Th2;

        per cases by A68, ENUMSET1:def 2;

          suppose

           A69: [n, m] = [1, 1];

          then

           A70: m = 1 by XTUPLE_0: 1;

          

           A71: n = 1 by A69, XTUPLE_0: 1;

          

          hence (G * (n,m)) = (f /. 4) by A70, MATRIX_0: 50

          .= |[(v1 . n), (v2 . m)]| by A39, A64, A66, A71, A70, EUCLID: 53;

        end;

          suppose

           A72: [n, m] = [1, 2];

          then

           A73: m = 2 by XTUPLE_0: 1;

          

           A74: n = 1 by A72, XTUPLE_0: 1;

          

          hence (G * (n,m)) = (f /. 1) by A73, MATRIX_0: 50

          .= |[(v1 . n), (v2 . m)]| by A39, A65, A74, A73, EUCLID: 53;

        end;

          suppose

           A75: [n, m] = [2, 1];

          then

           A76: m = 1 by XTUPLE_0: 1;

          

           A77: n = 2 by A75, XTUPLE_0: 1;

          

          hence (G * (n,m)) = (f /. 3) by A76, MATRIX_0: 50

          .= |[(v1 . n), (v2 . m)]| by A50, A64, A13, A7, A77, A76, EUCLID: 53;

        end;

          suppose

           A78: [n, m] = [2, 2];

          then

           A79: m = 2 by XTUPLE_0: 1;

          

           A80: n = 2 by A78, XTUPLE_0: 1;

          

          hence (G * (n,m)) = (f /. 2) by A79, MATRIX_0: 50

          .= |[(v1 . n), (v2 . m)]| by A50, A65, A4, A80, A79, EUCLID: 53;

        end;

      end;

      

       A81: ( width G) = 2 by MATRIX_0: 47

      .= ( len v2) by A63, FINSEQ_1: 44;

      ( len G) = 2 by MATRIX_0: 47

      .= ( len v1) by A38, FINSEQ_1: 44;

      then ( GoB (v1,v2)) = G by A81, A67, GOBOARD2:def 1;

      hence thesis by GOBOARD2:def 2;

    end;

    theorem :: SPRECT_3:37

    

     Th37: for f be rectangular special_circular_sequence holds ( LeftComp f) = { p : not (( W-bound ( L~ f)) <= (p `1 ) & (p `1 ) <= ( E-bound ( L~ f)) & ( S-bound ( L~ f)) <= (p `2 ) & (p `2 ) <= ( N-bound ( L~ f))) } & ( RightComp f) = { q : ( W-bound ( L~ f)) < (q `1 ) & (q `1 ) < ( E-bound ( L~ f)) & ( S-bound ( L~ f)) < (q `2 ) & (q `2 ) < ( N-bound ( L~ f)) }

    proof

      let f be rectangular special_circular_sequence;

      defpred U[ Element of ( TOP-REAL 2)] means not (( W-bound ( L~ f)) <= ($1 `1 ) & ($1 `1 ) <= ( E-bound ( L~ f)) & ( S-bound ( L~ f)) <= ($1 `2 ) & ($1 `2 ) <= ( N-bound ( L~ f)));

      defpred V[ Element of ( TOP-REAL 2)] means ( W-bound ( L~ f)) < ($1 `1 ) & ($1 `1 ) < ( E-bound ( L~ f)) & ( S-bound ( L~ f)) < ($1 `2 ) & ($1 `2 ) < ( N-bound ( L~ f));

      defpred W[ Element of ( TOP-REAL 2)] means ($1 `1 ) = ( W-bound ( L~ f)) & ($1 `2 ) <= ( N-bound ( L~ f)) & ($1 `2 ) >= ( S-bound ( L~ f)) or ($1 `1 ) <= ( E-bound ( L~ f)) & ($1 `1 ) >= ( W-bound ( L~ f)) & ($1 `2 ) = ( N-bound ( L~ f)) or ($1 `1 ) <= ( E-bound ( L~ f)) & ($1 `1 ) >= ( W-bound ( L~ f)) & ($1 `2 ) = ( S-bound ( L~ f)) or ($1 `1 ) = ( E-bound ( L~ f)) & ($1 `2 ) <= ( N-bound ( L~ f)) & ($1 `2 ) >= ( S-bound ( L~ f));

      set LC = { p : U[p] }, RC = { q : V[q] }, Lf = { p : W[p] };

      

       A1: ( S-bound ( L~ f)) < ( N-bound ( L~ f)) by SPRECT_1: 32;

      

       A2: Lf is Subset of ( TOP-REAL 2) from DOMAIN_1:sch 7;

      

       A3: RC is Subset of ( TOP-REAL 2) from DOMAIN_1:sch 7;

      

       A4: ( L~ f) = Lf by Th35;

      LC is Subset of ( TOP-REAL 2) from DOMAIN_1:sch 7;

      then

      reconsider Lc9 = LC, Rc9 = RC, Lf as Subset of ( TOP-REAL 2) by A3, A2;

      reconsider Lf as Subset of ( TOP-REAL 2);

      reconsider Lc9, Rc9 as Subset of ( TOP-REAL 2);

      

       A5: ( W-bound ( L~ f)) < ( E-bound ( L~ f)) by SPRECT_1: 31;

      then

      reconsider Lc = Lc9, Rc = Rc9 as Subset of (( TOP-REAL 2) | (Lf ` )) by A1, JORDAN1: 39, JORDAN1: 41;

      reconsider Lc, Rc as Subset of (( TOP-REAL 2) | (Lf ` ));

      

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

      Rc = Rc9;

      then Lc is a_component by A5, A1, JORDAN1: 36;

      then

       A7: Lc9 is_a_component_of (Lf ` ) by CONNSP_1:def 6;

      set p = (((1 / 2) * ((( GoB f) * (1,( width ( GoB f)))) + (( GoB f) * ((1 + 1),( width ( GoB f)))))) + |[ 0 , 1]|), q = ((1 / 2) * ((( GoB f) * (1,( width ( GoB f)))) + (( GoB f) * ((1 + 1),( width ( GoB f))))));

      

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

      

       A9: (p `2 ) = ((q `2 ) + ( |[ 0 , 1]| `2 )) by TOPREAL3: 2

      .= ((q `2 ) + 1) by EUCLID: 52;

      

       A10: ( GoB f) = (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) by Th36;

      then

       A11: (1 + 1) = ( width ( GoB f)) by MATRIX_0: 47;

      

      then (q `2 ) = (((1 / 2) * ((( GoB f) * (1,( width ( GoB f)))) + (f /. 2))) `2 ) by A10, MATRIX_0: 50

      .= (((1 / 2) * ((f /. 1) + (f /. 2))) `2 ) by A10, A11, MATRIX_0: 50

      .= ((1 / 2) * (((f /. 1) + (f /. 2)) `2 )) by TOPREAL3: 4

      .= ((1 / 2) * (((f /. 1) `2 ) + ((f /. 2) `2 ))) by TOPREAL3: 2

      .= ((1 / 2) * ((( N-min ( L~ f)) `2 ) + ((f /. 2) `2 ))) by SPRECT_1: 83

      .= ((1 / 2) * ((( N-min ( L~ f)) `2 ) + (( N-max ( L~ f)) `2 ))) by SPRECT_1: 84

      .= ((1 / 2) * (( N-bound ( L~ f)) + (( N-max ( L~ f)) `2 ))) by EUCLID: 52

      .= ((1 / 2) * (( N-bound ( L~ f)) + ( N-bound ( L~ f)))) by EUCLID: 52

      .= ( N-bound ( L~ f));

      then (p `2 ) > ( 0 + ( N-bound ( L~ f))) by A9, XREAL_1: 8;

      then

       A12: p in LC;

      

       A13: (1 + 1) = ( len ( GoB f)) by A10, MATRIX_0: 47;

      then

       A14: p in ( Int ( cell (( GoB f),1,(1 + 1)))) by A11, GOBOARD6: 32;

      

       A15: (f /. (1 + 1)) = (( GoB f) * ((1 + 1),(1 + 1))) by A10, MATRIX_0: 50;

      1 < ( width ( GoB f)) by GOBOARD7: 33;

      then

       A16: (1 + 1) <= ( width ( GoB f)) by NAT_1: 13;

      then

       A17: [(1 + 1), (1 + 1)] in ( Indices ( GoB f)) by A13, MATRIX_0: 30;

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

      then

       A18: [1, (1 + 1)] in ( Indices ( GoB f)) by A16, MATRIX_0: 30;

      

       A19: (f /. 1) = (( GoB f) * (1,(1 + 1))) by A10, MATRIX_0: 50;

      then ( right_cell (f,1)) = ( cell (( GoB f),1,1)) by A8, A18, A17, A15, GOBOARD5: 28;

      then

       A20: ( Int ( cell (( GoB f),1,1))) c= ( RightComp f) by GOBOARD9:def 2;

      ( left_cell (f,1)) = ( cell (( GoB f),1,(1 + 1))) by A8, A18, A19, A17, A15, GOBOARD5: 28;

      then ( Int ( cell (( GoB f),1,(1 + 1)))) c= ( LeftComp f) by GOBOARD9:def 1;

      then

       A21: LC meets ( LeftComp f) by A14, A12, XBOOLE_0: 3;

      

       A22: ((f /. 2) `1 ) = (( E-max ( L~ f)) `1 ) by SPRECT_1: 84

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

      set p = ((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (2,2))));

      

       A23: p in ( Int ( cell (( GoB f),1,1))) by A13, A11, GOBOARD6: 31;

      

       A24: p = ((1 / 2) * ((( GoB f) * (1,1)) + (f /. 2))) by A10, MATRIX_0: 50

      .= ((1 / 2) * ((f /. 4) + (f /. 2))) by A10, MATRIX_0: 50;

      

      then

       A25: (p `1 ) = ((1 / 2) * (((f /. 4) + (f /. 2)) `1 )) by TOPREAL3: 4

      .= ((1 / 2) * (((f /. 4) `1 ) + ((f /. 2) `1 ))) by TOPREAL3: 2

      .= (((1 / 2) * ((f /. 4) `1 )) + ((1 / 2) * ((f /. 2) `1 )));

      ( LeftComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1;

      hence ( LeftComp f) = LC by A4, A7, A21, GOBOARD9: 1;

      

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

      

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

      

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

      

       A29: ((f /. 4) `1 ) = (( W-min ( L~ f)) `1 ) by SPRECT_1: 86

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

      then ((1 / 2) * ((f /. 4) `1 )) < ((1 / 2) * ( E-bound ( L~ f))) by SPRECT_1: 31, XREAL_1: 68;

      then

       A30: (p `1 ) < ( E-bound ( L~ f)) by A27, A25, A22, XREAL_1: 6;

      

       A31: (p `2 ) = ((1 / 2) * (((f /. 4) + (f /. 2)) `2 )) by A24, TOPREAL3: 4

      .= ((1 / 2) * (((f /. 4) `2 ) + ((f /. 2) `2 ))) by TOPREAL3: 2

      .= (((1 / 2) * ((f /. 4) `2 )) + ((1 / 2) * ((f /. 2) `2 )));

      Lc = Lc9;

      then Rc is a_component by A5, A1, JORDAN1: 36;

      then

       A32: Rc9 is_a_component_of (Lf ` ) by CONNSP_1:def 6;

      

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

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

      

       A34: ((f /. 4) `2 ) = (( S-min ( L~ f)) `2 ) by SPRECT_1: 86

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

      then ((1 / 2) * ((f /. 4) `2 )) < ((1 / 2) * ( N-bound ( L~ f))) by SPRECT_1: 32, XREAL_1: 68;

      then

       A35: (p `2 ) < ( N-bound ( L~ f)) by A28, A31, A33, XREAL_1: 6;

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

      then

       A36: ( S-bound ( L~ f)) < (p `2 ) by A6, A31, A34, XREAL_1: 6;

      ((1 / 2) * ((f /. 2) `1 )) > ((1 / 2) * ( W-bound ( L~ f))) by A22, SPRECT_1: 31, XREAL_1: 68;

      then ( W-bound ( L~ f)) < (p `1 ) by A26, A25, A29, XREAL_1: 6;

      then p in RC by A30, A36, A35;

      then

       A37: RC meets ( RightComp f) by A23, A20, XBOOLE_0: 3;

      ( RightComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 2;

      hence thesis by A4, A32, A37, GOBOARD9: 1;

    end;

    registration

      cluster clockwise_oriented for rectangular special_circular_sequence;

      existence

      proof

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

        ( SpStSeq C) is clockwise_oriented;

        hence thesis;

      end;

    end

    registration

      cluster -> clockwise_oriented for rectangular special_circular_sequence;

      coherence

      proof

        let f be rectangular special_circular_sequence;

        ex D be non vertical non horizontal non empty compact Subset of ( TOP-REAL 2) st f = ( SpStSeq D) by SPRECT_1:def 2;

        hence thesis;

      end;

    end

    theorem :: SPRECT_3:38

    for f be rectangular special_circular_sequence, g be S-Sequence_in_R2 st (g /. 1) in ( LeftComp f) & (g /. ( len g)) in ( RightComp f) holds ( Last_Point (( L~ g),(g /. 1),(g /. ( len g)),( L~ f))) <> ( NW-corner ( L~ f))

    proof

      let f be rectangular special_circular_sequence, g be S-Sequence_in_R2 such that

       A1: (g /. 1) in ( LeftComp f) and

       A2: (g /. ( len g)) in ( RightComp f);

      

       A3: ( L~ f) meets ( L~ g) by A1, A2, Th33;

      assume

       A4: ( Last_Point (( L~ g),(g /. 1),(g /. ( len g)),( L~ f))) = ( NW-corner ( L~ f));

      set nw = ( NW-corner ( L~ f)), inw = ( Index (nw,g));

      

       A5: ( len g) in ( dom g) by FINSEQ_5: 6;

      then

       A6: (g . ( len g)) = (g /. ( len g)) by PARTFUN1:def 6;

      

       A7: 1 <= (inw + 1) by NAT_1: 11;

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

      then

       A8: nw in (( L~ g) /\ ( L~ f)) by A3, A4, JORDAN5C:def 2;

      then

       A9: nw in ( L~ g) by XBOOLE_0:def 4;

      then

       A10: 1 <= inw by JORDAN3: 8;

      

       A11: nw in ( LSeg (g,inw)) by A9, JORDAN3: 9;

      

       A12: inw < ( len g) by A9, JORDAN3: 8;

      then

       A13: (inw + 1) <= ( len g) by NAT_1: 13;

      then

       A14: (inw + 1) in ( dom g) by A7, FINSEQ_3: 25;

      

       A15: ( L~ f) misses ( RightComp f) by Th25;

       A16:

      now

        

         A17: ( len g) >= 1 by A13, A7, XXREAL_0: 2;

        assume nw <> (g . (inw + 1));

        then

         A18: nw <> (g /. (inw + 1)) by A14, PARTFUN1:def 6;

        per cases ;

          suppose

           A19: (g /. (inw + 1)) in ( L~ f);

          then (inw + 1) <> ( len g) by A2, A15, XBOOLE_0: 3;

          then (inw + 1) < ( len g) by A13, XXREAL_0: 1;

          then

           A20: ((inw + 1) + 1) <= ( len g) by NAT_1: 13;

          then (g /. (inw + 1)) in ( LSeg (g,(inw + 1))) by A7, TOPREAL1: 21;

          then inw >= (inw + 1) by A3, A4, A10, A13, A11, A7, A18, A19, A20, JORDAN5C: 28;

          hence contradiction by XREAL_1: 29;

        end;

          suppose

           A21: not (g /. (inw + 1)) in ( L~ f);

           A22:

          now

            assume

             A23: (g /. (inw + 1)) in ( RightComp f);

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

            then

             A24: ex q st (g /. (inw + 1)) = q & ( W-bound ( L~ f)) < (q `1 ) & (q `1 ) < ( E-bound ( L~ f)) & ( S-bound ( L~ f)) < (q `2 ) & (q `2 ) < ( N-bound ( L~ f)) by A23;

            

             A25: ( LSeg (g,inw)) is vertical or ( LSeg (g,inw)) is horizontal by SPPOL_1: 19;

            ( LSeg (g,inw)) = ( LSeg ((g /. inw),(g /. (inw + 1)))) by A10, A13, TOPREAL1:def 3;

            then ((g /. (inw + 1)) `1 ) = (nw `1 ) or ((g /. (inw + 1)) `2 ) = (nw `2 ) by A11, A25, SPPOL_1: 40, SPPOL_1: 41;

            hence contradiction by A24, EUCLID: 52;

          end;

          then

          reconsider m = ( mid (g,(inw + 1),( len g))) as S-Sequence_in_R2 by A2, A13, A7, A17, JORDAN3: 6;

          

           A26: (inw + 1) < ( len g) by A2, A13, A22, XXREAL_0: 1;

          (g /. (inw + 1)) in (( L~ f) ` ) by A21, SUBSET_1: 29;

          then (g /. (inw + 1)) in (( LeftComp f) \/ ( RightComp f)) by GOBRD12: 10;

          then (g /. (inw + 1)) in ( LeftComp f) by A22, XBOOLE_0:def 3;

          then

           A27: (m /. 1) in ( LeftComp f) by A5, A14, SPRECT_2: 8;

          (m /. ( len m)) in ( RightComp f) by A2, A5, A14, SPRECT_2: 9;

          then ( L~ f) meets ( L~ m) by A27, Th33;

          then

          consider q be object such that

           A28: q in ( L~ f) and

           A29: q in ( L~ m) by XBOOLE_0: 3;

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

          consider i such that

           A30: 1 <= i and

           A31: (i + 1) <= ( len m) and

           A32: q in ( LSeg (m,i)) by A29, SPPOL_2: 13;

          set j = ((i + (inw + 1)) -' 1);

          

           A33: j = (((i + inw) + 1) -' 1)

          .= (i + inw) by NAT_D: 34;

          

           A34: ( len m) = ((( len g) -' (inw + 1)) + 1) by A13, A7, JORDAN4: 8;

          then ( len m) = (( len g) -' inw) by A9, JORDAN3: 8, NAT_2: 7;

          then (( len m) + inw) = ( len g) by A12, XREAL_1: 235;

          then ((i + 1) + inw) <= ( len g) by A31, XREAL_1: 6;

          then

           A35: (j + 1) <= ( len g) by A33;

          i < ( len m) by A31, NAT_1: 13;

          then

           A36: ( LSeg (m,i)) = ( LSeg (g,((i + (inw + 1)) -' 1))) by A7, A26, A30, A34, JORDAN4: 19;

          

           A37: j >= (inw + 1) by A30, A33, XREAL_1: 6;

           A38:

          now

            assume nw = q;

            then

             A39: nw in (( LSeg (g,inw)) /\ ( LSeg (g,j))) by A11, A32, A36, XBOOLE_0:def 4;

            then

             A40: ( LSeg (g,inw)) meets ( LSeg (g,j));

            per cases by A37, XXREAL_0: 1;

              suppose

               A41: (inw + 1) = j;

              ((inw + 1) + 1) <= ( len g) by A26, NAT_1: 13;

              then (inw + (1 + 1)) <= ( len g);

              then (( LSeg (g,inw)) /\ ( LSeg (g,(inw + 1)))) = {(g /. (inw + 1))} by A10, TOPREAL1:def 6;

              hence contradiction by A18, A39, A41, TARSKI:def 1;

            end;

              suppose (inw + 1) < j;

              hence contradiction by A40, TOPREAL1:def 7;

            end;

          end;

          ( 0 + 1) <= j by A30, A33, XREAL_1: 7;

          then inw >= j by A3, A4, A10, A13, A11, A28, A32, A36, A35, A38, JORDAN5C: 28;

          then inw >= (inw + 1) by A37, XXREAL_0: 2;

          hence contradiction by XREAL_1: 29;

        end;

      end;

      nw in ( L~ f) by A8, XBOOLE_0:def 4;

      then nw <> (g . ( len g)) by A2, A15, A6, XBOOLE_0: 3;

      then

       A42: (inw + 1) < ( len g) by A13, A16, XXREAL_0: 1;

      then

       A43: ((inw + 1) + 1) <= ( len g) by NAT_1: 13;

      then (g /. (inw + 1)) in ( LSeg (g,(inw + 1))) by A7, TOPREAL1: 21;

      then

       A44: nw in ( LSeg (g,(inw + 1))) by A14, A16, PARTFUN1:def 6;

      

       A45: 1 <= ((inw + 1) + 1) by NAT_1: 11;

      then

       A46: ( len g) >= 1 by A43, XXREAL_0: 2;

      

       A47: ((inw + 1) + 1) in ( dom g) by A43, A45, FINSEQ_3: 25;

      (inw + 1) < ((inw + 1) + 1) by NAT_1: 13;

      then

       A48: nw <> (g . ((inw + 1) + 1)) by A14, A16, A47, FUNCT_1:def 4;

      then

       A49: nw <> (g /. ((inw + 1) + 1)) by A47, PARTFUN1:def 6;

      per cases ;

        suppose

         A50: (g /. ((inw + 1) + 1)) in ( L~ f);

        

         A51: nw <> (g /. ((inw + 1) + 1)) by A47, A48, PARTFUN1:def 6;

        ((inw + 1) + 1) <> ( len g) by A2, A15, A50, XBOOLE_0: 3;

        then ((inw + 1) + 1) < ( len g) by A43, XXREAL_0: 1;

        then

         A52: (((inw + 1) + 1) + 1) <= ( len g) by NAT_1: 13;

        then (g /. ((inw + 1) + 1)) in ( LSeg (g,((inw + 1) + 1))) by A45, TOPREAL1: 21;

        then (inw + 1) >= ((inw + 1) + 1) by A3, A4, A7, A43, A45, A44, A50, A52, A51, JORDAN5C: 28;

        hence contradiction by XREAL_1: 29;

      end;

        suppose

         A53: not (g /. ((inw + 1) + 1)) in ( L~ f);

         A54:

        now

          assume

           A55: (g /. ((inw + 1) + 1)) in ( RightComp f);

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

          then

           A56: ex q st (g /. ((inw + 1) + 1)) = q & ( W-bound ( L~ f)) < (q `1 ) & (q `1 ) < ( E-bound ( L~ f)) & ( S-bound ( L~ f)) < (q `2 ) & (q `2 ) < ( N-bound ( L~ f)) by A55;

          

           A57: ( LSeg (g,(inw + 1))) is vertical or ( LSeg (g,(inw + 1))) is horizontal by SPPOL_1: 19;

          ( LSeg (g,(inw + 1))) = ( LSeg ((g /. (inw + 1)),(g /. ((inw + 1) + 1)))) by A7, A43, TOPREAL1:def 3;

          then ((g /. ((inw + 1) + 1)) `1 ) = (nw `1 ) or ((g /. ((inw + 1) + 1)) `2 ) = (nw `2 ) by A44, A57, SPPOL_1: 40, SPPOL_1: 41;

          hence contradiction by A56, EUCLID: 52;

        end;

        then

        reconsider m = ( mid (g,((inw + 1) + 1),( len g))) as S-Sequence_in_R2 by A2, A43, A45, A46, JORDAN3: 6;

        

         A58: ((inw + 1) + 1) < ( len g) by A2, A43, A54, XXREAL_0: 1;

        (g /. ((inw + 1) + 1)) in (( L~ f) ` ) by A53, SUBSET_1: 29;

        then (g /. ((inw + 1) + 1)) in (( LeftComp f) \/ ( RightComp f)) by GOBRD12: 10;

        then (g /. ((inw + 1) + 1)) in ( LeftComp f) by A54, XBOOLE_0:def 3;

        then

         A59: (m /. 1) in ( LeftComp f) by A5, A47, SPRECT_2: 8;

        (m /. ( len m)) in ( RightComp f) by A2, A5, A47, SPRECT_2: 9;

        then ( L~ f) meets ( L~ m) by A59, Th33;

        then

        consider q be object such that

         A60: q in ( L~ f) and

         A61: q in ( L~ m) by XBOOLE_0: 3;

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

        consider i such that

         A62: 1 <= i and

         A63: (i + 1) <= ( len m) and

         A64: q in ( LSeg (m,i)) by A61, SPPOL_2: 13;

        set j = ((i + ((inw + 1) + 1)) -' 1);

        

         A65: ( len m) = ((( len g) -' ((inw + 1) + 1)) + 1) by A43, A45, JORDAN4: 8;

        then ( len m) = (( len g) -' (inw + 1)) by A42, NAT_2: 7;

        then (( len m) + (inw + 1)) = ( len g) by A13, XREAL_1: 235;

        then ((i + 1) + (inw + 1)) <= ( len g) by A63, XREAL_1: 6;

        then

         A66: (((i + 1) + inw) + 1) <= ( len g);

        i < ( len m) by A63, NAT_1: 13;

        then

         A67: ( LSeg (m,i)) = ( LSeg (g,((i + ((inw + 1) + 1)) -' 1))) by A45, A58, A62, A65, JORDAN4: 19;

        

         A68: j = ((((i + inw) + 1) + 1) -' 1)

        .= ((i + inw) + 1) by NAT_D: 34;

        then j = (i + (inw + 1));

        then

         A69: j >= ((inw + 1) + 1) by A62, XREAL_1: 6;

         A70:

        now

          assume nw = q;

          then

           A71: nw in (( LSeg (g,(inw + 1))) /\ ( LSeg (g,j))) by A44, A64, A67, XBOOLE_0:def 4;

          then

           A72: ( LSeg (g,(inw + 1))) meets ( LSeg (g,j));

          per cases by A69, XXREAL_0: 1;

            suppose

             A73: ((inw + 1) + 1) = j;

            (((inw + 1) + 1) + 1) <= ( len g) by A58, NAT_1: 13;

            then ((inw + 1) + (1 + 1)) <= ( len g);

            then (( LSeg (g,(inw + 1))) /\ ( LSeg (g,((inw + 1) + 1)))) = {(g /. ((inw + 1) + 1))} by A7, TOPREAL1:def 6;

            hence contradiction by A49, A71, A73, TARSKI:def 1;

          end;

            suppose ((inw + 1) + 1) < j;

            hence contradiction by A72, TOPREAL1:def 7;

          end;

        end;

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

        then (inw + 1) >= j by A3, A4, A7, A43, A44, A60, A64, A67, A68, A66, A70, JORDAN5C: 28;

        then (inw + 1) >= ((inw + 1) + 1) by A69, XXREAL_0: 2;

        hence contradiction by XREAL_1: 29;

      end;

    end;

    theorem :: SPRECT_3:39

    for f be rectangular special_circular_sequence, g be S-Sequence_in_R2 st (g /. 1) in ( LeftComp f) & (g /. ( len g)) in ( RightComp f) holds ( Last_Point (( L~ g),(g /. 1),(g /. ( len g)),( L~ f))) <> ( SE-corner ( L~ f))

    proof

      let f be rectangular special_circular_sequence, g be S-Sequence_in_R2 such that

       A1: (g /. 1) in ( LeftComp f) and

       A2: (g /. ( len g)) in ( RightComp f);

      

       A3: ( L~ f) meets ( L~ g) by A1, A2, Th33;

      assume

       A4: ( Last_Point (( L~ g),(g /. 1),(g /. ( len g)),( L~ f))) = ( SE-corner ( L~ f));

      set se = ( SE-corner ( L~ f)), ise = ( Index (se,g));

      

       A5: ( len g) in ( dom g) by FINSEQ_5: 6;

      then

       A6: (g . ( len g)) = (g /. ( len g)) by PARTFUN1:def 6;

      

       A7: 1 <= (ise + 1) by NAT_1: 11;

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

      then

       A8: se in (( L~ g) /\ ( L~ f)) by A3, A4, JORDAN5C:def 2;

      then

       A9: se in ( L~ g) by XBOOLE_0:def 4;

      then

       A10: 1 <= ise by JORDAN3: 8;

      

       A11: se in ( LSeg (g,ise)) by A9, JORDAN3: 9;

      

       A12: ise < ( len g) by A9, JORDAN3: 8;

      then

       A13: (ise + 1) <= ( len g) by NAT_1: 13;

      then

       A14: (ise + 1) in ( dom g) by A7, FINSEQ_3: 25;

      

       A15: ( L~ f) misses ( RightComp f) by Th25;

       A16:

      now

        

         A17: ( len g) >= 1 by A13, A7, XXREAL_0: 2;

        assume se <> (g . (ise + 1));

        then

         A18: se <> (g /. (ise + 1)) by A14, PARTFUN1:def 6;

        per cases ;

          suppose

           A19: (g /. (ise + 1)) in ( L~ f);

          then (ise + 1) <> ( len g) by A2, A15, XBOOLE_0: 3;

          then (ise + 1) < ( len g) by A13, XXREAL_0: 1;

          then

           A20: ((ise + 1) + 1) <= ( len g) by NAT_1: 13;

          then (g /. (ise + 1)) in ( LSeg (g,(ise + 1))) by A7, TOPREAL1: 21;

          then ise >= (ise + 1) by A3, A4, A10, A13, A11, A7, A18, A19, A20, JORDAN5C: 28;

          hence contradiction by XREAL_1: 29;

        end;

          suppose

           A21: not (g /. (ise + 1)) in ( L~ f);

           A22:

          now

            assume

             A23: (g /. (ise + 1)) in ( RightComp f);

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

            then

             A24: ex q st (g /. (ise + 1)) = q & ( W-bound ( L~ f)) < (q `1 ) & (q `1 ) < ( E-bound ( L~ f)) & ( S-bound ( L~ f)) < (q `2 ) & (q `2 ) < ( N-bound ( L~ f)) by A23;

            

             A25: ( LSeg (g,ise)) is vertical or ( LSeg (g,ise)) is horizontal by SPPOL_1: 19;

            ( LSeg (g,ise)) = ( LSeg ((g /. ise),(g /. (ise + 1)))) by A10, A13, TOPREAL1:def 3;

            then ((g /. (ise + 1)) `1 ) = (se `1 ) or ((g /. (ise + 1)) `2 ) = (se `2 ) by A11, A25, SPPOL_1: 40, SPPOL_1: 41;

            hence contradiction by A24, EUCLID: 52;

          end;

          then

          reconsider m = ( mid (g,(ise + 1),( len g))) as S-Sequence_in_R2 by A2, A13, A7, A17, JORDAN3: 6;

          

           A26: (ise + 1) < ( len g) by A2, A13, A22, XXREAL_0: 1;

          (g /. (ise + 1)) in (( L~ f) ` ) by A21, SUBSET_1: 29;

          then (g /. (ise + 1)) in (( LeftComp f) \/ ( RightComp f)) by GOBRD12: 10;

          then (g /. (ise + 1)) in ( LeftComp f) by A22, XBOOLE_0:def 3;

          then

           A27: (m /. 1) in ( LeftComp f) by A5, A14, SPRECT_2: 8;

          (m /. ( len m)) in ( RightComp f) by A2, A5, A14, SPRECT_2: 9;

          then ( L~ f) meets ( L~ m) by A27, Th33;

          then

          consider q be object such that

           A28: q in ( L~ f) and

           A29: q in ( L~ m) by XBOOLE_0: 3;

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

          consider i such that

           A30: 1 <= i and

           A31: (i + 1) <= ( len m) and

           A32: q in ( LSeg (m,i)) by A29, SPPOL_2: 13;

          set j = ((i + (ise + 1)) -' 1);

          

           A33: j = (((i + ise) + 1) -' 1)

          .= (i + ise) by NAT_D: 34;

          

           A34: ( len m) = ((( len g) -' (ise + 1)) + 1) by A13, A7, JORDAN4: 8;

          then ( len m) = (( len g) -' ise) by A9, JORDAN3: 8, NAT_2: 7;

          then (( len m) + ise) = ( len g) by A12, XREAL_1: 235;

          then ((i + 1) + ise) <= ( len g) by A31, XREAL_1: 6;

          then

           A35: (j + 1) <= ( len g) by A33;

          i < ( len m) by A31, NAT_1: 13;

          then

           A36: ( LSeg (m,i)) = ( LSeg (g,((i + (ise + 1)) -' 1))) by A7, A26, A30, A34, JORDAN4: 19;

          

           A37: j >= (ise + 1) by A30, A33, XREAL_1: 6;

           A38:

          now

            assume se = q;

            then

             A39: se in (( LSeg (g,ise)) /\ ( LSeg (g,j))) by A11, A32, A36, XBOOLE_0:def 4;

            then

             A40: ( LSeg (g,ise)) meets ( LSeg (g,j));

            per cases by A37, XXREAL_0: 1;

              suppose

               A41: (ise + 1) = j;

              ((ise + 1) + 1) <= ( len g) by A26, NAT_1: 13;

              then (ise + (1 + 1)) <= ( len g);

              then (( LSeg (g,ise)) /\ ( LSeg (g,(ise + 1)))) = {(g /. (ise + 1))} by A10, TOPREAL1:def 6;

              hence contradiction by A18, A39, A41, TARSKI:def 1;

            end;

              suppose (ise + 1) < j;

              hence contradiction by A40, TOPREAL1:def 7;

            end;

          end;

          ( 0 + 1) <= j by A30, A33, XREAL_1: 7;

          then ise >= j by A3, A4, A10, A13, A11, A28, A32, A36, A35, A38, JORDAN5C: 28;

          then ise >= (ise + 1) by A37, XXREAL_0: 2;

          hence contradiction by XREAL_1: 29;

        end;

      end;

      se in ( L~ f) by A8, XBOOLE_0:def 4;

      then se <> (g . ( len g)) by A2, A15, A6, XBOOLE_0: 3;

      then

       A42: (ise + 1) < ( len g) by A13, A16, XXREAL_0: 1;

      then

       A43: ((ise + 1) + 1) <= ( len g) by NAT_1: 13;

      then (g /. (ise + 1)) in ( LSeg (g,(ise + 1))) by A7, TOPREAL1: 21;

      then

       A44: se in ( LSeg (g,(ise + 1))) by A14, A16, PARTFUN1:def 6;

      

       A45: 1 <= ((ise + 1) + 1) by NAT_1: 11;

      then

       A46: ( len g) >= 1 by A43, XXREAL_0: 2;

      

       A47: ((ise + 1) + 1) in ( dom g) by A43, A45, FINSEQ_3: 25;

      (ise + 1) < ((ise + 1) + 1) by NAT_1: 13;

      then

       A48: se <> (g . ((ise + 1) + 1)) by A14, A16, A47, FUNCT_1:def 4;

      then

       A49: se <> (g /. ((ise + 1) + 1)) by A47, PARTFUN1:def 6;

      per cases ;

        suppose

         A50: (g /. ((ise + 1) + 1)) in ( L~ f);

        

         A51: se <> (g /. ((ise + 1) + 1)) by A47, A48, PARTFUN1:def 6;

        ((ise + 1) + 1) <> ( len g) by A2, A15, A50, XBOOLE_0: 3;

        then ((ise + 1) + 1) < ( len g) by A43, XXREAL_0: 1;

        then

         A52: (((ise + 1) + 1) + 1) <= ( len g) by NAT_1: 13;

        then (g /. ((ise + 1) + 1)) in ( LSeg (g,((ise + 1) + 1))) by A45, TOPREAL1: 21;

        then (ise + 1) >= ((ise + 1) + 1) by A3, A4, A7, A43, A45, A44, A50, A52, A51, JORDAN5C: 28;

        hence contradiction by XREAL_1: 29;

      end;

        suppose

         A53: not (g /. ((ise + 1) + 1)) in ( L~ f);

         A54:

        now

          assume

           A55: (g /. ((ise + 1) + 1)) in ( RightComp f);

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

          then

           A56: ex q st (g /. ((ise + 1) + 1)) = q & ( W-bound ( L~ f)) < (q `1 ) & (q `1 ) < ( E-bound ( L~ f)) & ( S-bound ( L~ f)) < (q `2 ) & (q `2 ) < ( N-bound ( L~ f)) by A55;

          

           A57: ( LSeg (g,(ise + 1))) is vertical or ( LSeg (g,(ise + 1))) is horizontal by SPPOL_1: 19;

          ( LSeg (g,(ise + 1))) = ( LSeg ((g /. (ise + 1)),(g /. ((ise + 1) + 1)))) by A7, A43, TOPREAL1:def 3;

          then ((g /. ((ise + 1) + 1)) `1 ) = (se `1 ) or ((g /. ((ise + 1) + 1)) `2 ) = (se `2 ) by A44, A57, SPPOL_1: 40, SPPOL_1: 41;

          hence contradiction by A56, EUCLID: 52;

        end;

        then

        reconsider m = ( mid (g,((ise + 1) + 1),( len g))) as S-Sequence_in_R2 by A2, A43, A45, A46, JORDAN3: 6;

        

         A58: ((ise + 1) + 1) < ( len g) by A2, A43, A54, XXREAL_0: 1;

        (g /. ((ise + 1) + 1)) in (( L~ f) ` ) by A53, SUBSET_1: 29;

        then (g /. ((ise + 1) + 1)) in (( LeftComp f) \/ ( RightComp f)) by GOBRD12: 10;

        then (g /. ((ise + 1) + 1)) in ( LeftComp f) by A54, XBOOLE_0:def 3;

        then

         A59: (m /. 1) in ( LeftComp f) by A5, A47, SPRECT_2: 8;

        (m /. ( len m)) in ( RightComp f) by A2, A5, A47, SPRECT_2: 9;

        then ( L~ f) meets ( L~ m) by A59, Th33;

        then

        consider q be object such that

         A60: q in ( L~ f) and

         A61: q in ( L~ m) by XBOOLE_0: 3;

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

        consider i such that

         A62: 1 <= i and

         A63: (i + 1) <= ( len m) and

         A64: q in ( LSeg (m,i)) by A61, SPPOL_2: 13;

        set j = ((i + ((ise + 1) + 1)) -' 1);

        

         A65: ( len m) = ((( len g) -' ((ise + 1) + 1)) + 1) by A43, A45, JORDAN4: 8;

        then ( len m) = (( len g) -' (ise + 1)) by A42, NAT_2: 7;

        then (( len m) + (ise + 1)) = ( len g) by A13, XREAL_1: 235;

        then ((i + 1) + (ise + 1)) <= ( len g) by A63, XREAL_1: 6;

        then

         A66: (((i + 1) + ise) + 1) <= ( len g);

        i < ( len m) by A63, NAT_1: 13;

        then

         A67: ( LSeg (m,i)) = ( LSeg (g,((i + ((ise + 1) + 1)) -' 1))) by A45, A58, A62, A65, JORDAN4: 19;

        

         A68: j = ((((i + ise) + 1) + 1) -' 1)

        .= ((i + ise) + 1) by NAT_D: 34;

        then j = (i + (ise + 1));

        then

         A69: j >= ((ise + 1) + 1) by A62, XREAL_1: 6;

         A70:

        now

          assume se = q;

          then

           A71: se in (( LSeg (g,(ise + 1))) /\ ( LSeg (g,j))) by A44, A64, A67, XBOOLE_0:def 4;

          then

           A72: ( LSeg (g,(ise + 1))) meets ( LSeg (g,j));

          per cases by A69, XXREAL_0: 1;

            suppose

             A73: ((ise + 1) + 1) = j;

            (((ise + 1) + 1) + 1) <= ( len g) by A58, NAT_1: 13;

            then ((ise + 1) + (1 + 1)) <= ( len g);

            then (( LSeg (g,(ise + 1))) /\ ( LSeg (g,((ise + 1) + 1)))) = {(g /. ((ise + 1) + 1))} by A7, TOPREAL1:def 6;

            hence contradiction by A49, A71, A73, TARSKI:def 1;

          end;

            suppose ((ise + 1) + 1) < j;

            hence contradiction by A72, TOPREAL1:def 7;

          end;

        end;

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

        then (ise + 1) >= j by A3, A4, A7, A43, A44, A60, A64, A67, A68, A66, A70, JORDAN5C: 28;

        then (ise + 1) >= ((ise + 1) + 1) by A69, XXREAL_0: 2;

        hence contradiction by XREAL_1: 29;

      end;

    end;

    theorem :: SPRECT_3:40

    

     Th40: for f be rectangular special_circular_sequence, p be Point of ( TOP-REAL 2) st ( W-bound ( L~ f)) > (p `1 ) or (p `1 ) > ( E-bound ( L~ f)) or ( S-bound ( L~ f)) > (p `2 ) or (p `2 ) > ( N-bound ( L~ f)) holds p in ( LeftComp f)

    proof

      let f be rectangular special_circular_sequence, p be Point of ( TOP-REAL 2);

      ( LeftComp f) = { q : not (( W-bound ( L~ f)) <= (q `1 ) & (q `1 ) <= ( E-bound ( L~ f)) & ( S-bound ( L~ f)) <= (q `2 ) & (q `2 ) <= ( N-bound ( L~ f))) } by Th37;

      hence thesis;

    end;

    theorem :: SPRECT_3:41

    for f be clockwise_oriented non constant standard special_circular_sequence st (f /. 1) = ( N-min ( L~ f)) holds ( LeftComp ( SpStSeq ( L~ f))) c= ( LeftComp f)

    proof

      let f be clockwise_oriented non constant standard special_circular_sequence such that

       A1: (f /. 1) = ( N-min ( L~ f));

      defpred X[ Element of ( TOP-REAL 2)] means ($1 `2 ) < ( S-bound ( L~ f));

      reconsider P1 = { p : X[p] } as Subset of ( TOP-REAL 2) from DOMAIN_1:sch 7;

      defpred X[ Element of ( TOP-REAL 2)] means ($1 `2 ) > ( N-bound ( L~ f));

      reconsider P2 = { p : X[p] } as Subset of ( TOP-REAL 2) from DOMAIN_1:sch 7;

      defpred X[ Element of ( TOP-REAL 2)] means ($1 `1 ) > ( E-bound ( L~ f));

      reconsider P3 = { p : X[p] } as Subset of ( TOP-REAL 2) from DOMAIN_1:sch 7;

      defpred X[ Element of ( TOP-REAL 2)] means ($1 `1 ) < ( W-bound ( L~ f));

      reconsider P4 = { p : X[p] } as Subset of ( TOP-REAL 2) from DOMAIN_1:sch 7;

      

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

      for p st p in P2 holds (p `2 ) > ((( GoB f) * (1,( width ( GoB f)))) `2 )

      proof

        let p;

        assume p in P2;

        then ex q st p = q & (q `2 ) > ( N-bound ( L~ f));

        hence thesis by JORDAN5D: 40;

      end;

      then

       A3: P2 misses ( L~ f) by GOBOARD8: 24;

      

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

      

       A5: ((( width ( GoB f)) -' 1) + 1) = ( width ( GoB f)) by GOBRD11: 34, XREAL_1: 235;

      consider i such that

       A6: 1 <= i and

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

       A8: ( N-min ( L~ f)) = (( GoB f) * (i,( width ( GoB f)))) by Th28;

      

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

      

       A10: i in ( dom ( GoB f)) by A6, A7, FINSEQ_3: 25;

      then

       A11: (f /. 2) = (( GoB f) * ((i + 1),( width ( GoB f)))) by A1, A8, Th29;

      

       A12: ( width ( GoB f)) >= 1 by GOBRD11: 34;

      then

       A13: [i, ( width ( GoB f))] in ( Indices ( GoB f)) by A6, A7, MATRIX_0: 30;

      

       A14: 1 <= (i + 1) by A6, NAT_1: 13;

      

      then

       A15: ((f /. 2) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A11, A12, A9, GOBOARD5: 1

      .= (( N-min ( L~ f)) `2 ) by A6, A7, A8, A12, GOBOARD5: 1

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

      set a = (((1 / 2) * ((( GoB f) * (i,( width ( GoB f)))) + (( GoB f) * ((i + 1),( width ( GoB f)))))) + |[ 0 , 1]|), q = ((1 / 2) * ((( GoB f) * (i,( width ( GoB f)))) + (( GoB f) * ((i + 1),( width ( GoB f))))));

      

       A16: (a `2 ) = ((q `2 ) + ( |[ 0 , 1]| `2 )) by TOPREAL3: 2

      .= ((q `2 ) + 1) by EUCLID: 52;

      (q `2 ) = (((1 / 2) * ((( GoB f) * (i,( width ( GoB f)))) + (f /. 2))) `2 ) by A1, A8, A10, Th29

      .= ((1 / 2) * (((f /. 1) + (f /. 2)) `2 )) by A1, A8, TOPREAL3: 4

      .= ((1 / 2) * (((f /. 1) `2 ) + ((f /. 2) `2 ))) by TOPREAL3: 2

      .= ((1 / 2) * (( N-bound ( L~ f)) + ( N-bound ( L~ f)))) by A1, A15, EUCLID: 52

      .= ( N-bound ( L~ f));

      then (a `2 ) > ( 0 + ( N-bound ( L~ f))) by A16, XREAL_1: 8;

      then

       A17: (a `2 ) > ( N-bound ( L~ ( SpStSeq ( L~ f)))) by SPRECT_1: 60;

      ( LeftComp ( SpStSeq ( L~ f))) = { p : not (( W-bound ( L~ ( SpStSeq ( L~ f)))) <= (p `1 ) & (p `1 ) <= ( E-bound ( L~ ( SpStSeq ( L~ f)))) & ( S-bound ( L~ ( SpStSeq ( L~ f)))) <= (p `2 ) & (p `2 ) <= ( N-bound ( L~ ( SpStSeq ( L~ f))))) } by Th37;

      then

       A18: a in ( LeftComp ( SpStSeq ( L~ f))) by A17;

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

      then ( left_cell (f,1)) = ( cell (( GoB f),i,( width ( GoB f)))) by A1, A8, A11, A5, A4, A13, GOBOARD5: 28;

      then

       A19: ( Int ( cell (( GoB f),i,( width ( GoB f))))) c= ( LeftComp f) by GOBOARD9:def 1;

      a in ( Int ( cell (( GoB f),i,( width ( GoB f))))) by A6, A9, GOBOARD6: 32;

      then

       A20: ( LeftComp f) meets ( LeftComp ( SpStSeq ( L~ f))) by A19, A18, XBOOLE_0: 3;

      

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

      for p st p in P4 holds (p `1 ) < ((( GoB f) * (1,1)) `1 )

      proof

        let p;

        assume p in P4;

        then ex q st p = q & (q `1 ) < ( W-bound ( L~ f));

        hence thesis by JORDAN5D: 37;

      end;

      then

       A22: P4 misses ( L~ f) by GOBOARD8: 21;

      for p st p in P3 holds (p `1 ) > ((( GoB f) * (( len ( GoB f)),1)) `1 )

      proof

        let p;

        assume p in P3;

        then ex q st p = q & (q `1 ) > ( E-bound ( L~ f));

        hence thesis by JORDAN5D: 39;

      end;

      then P3 misses ( L~ f) by GOBOARD8: 22;

      then

       A23: (P3 \/ P4) misses ( L~ f) by A22, XBOOLE_1: 70;

      ( LeftComp ( SpStSeq ( L~ f))) is_a_component_of (( L~ ( SpStSeq ( L~ f))) ` ) by GOBOARD9:def 1;

      then

      consider B1 be Subset of (( TOP-REAL 2) | (( L~ ( SpStSeq ( L~ f))) ` )) such that

       A24: B1 = ( LeftComp ( SpStSeq ( L~ f))) and

       A25: B1 is a_component by CONNSP_1:def 6;

      B1 is connected by A25, CONNSP_1:def 5;

      then

       A26: ( LeftComp ( SpStSeq ( L~ f))) is connected by A24, CONNSP_1: 23;

      

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

      

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

      

       A29: ( LeftComp ( SpStSeq ( L~ f))) = ((P1 \/ P2) \/ (P3 \/ P4))

      proof

        thus ( LeftComp ( SpStSeq ( L~ f))) c= ((P1 \/ P2) \/ (P3 \/ P4))

        proof

          let x be object;

          assume x in ( LeftComp ( SpStSeq ( L~ f)));

          then x in { p : not (( W-bound ( L~ f)) <= (p `1 ) & (p `1 ) <= ( E-bound ( L~ f)) & ( S-bound ( L~ f)) <= (p `2 ) & (p `2 ) <= ( N-bound ( L~ f))) } by A28, A2, A21, A27, Th37;

          then ex p st p = x & not (( W-bound ( L~ f)) <= (p `1 ) & (p `1 ) <= ( E-bound ( L~ f)) & ( S-bound ( L~ f)) <= (p `2 ) & (p `2 ) <= ( N-bound ( L~ f)));

          then x in P1 or x in P2 or x in P3 or x in P4;

          then x in (P1 \/ P2) or x in (P3 \/ P4) by XBOOLE_0:def 3;

          hence thesis by XBOOLE_0:def 3;

        end;

        let x be object;

        assume x in ((P1 \/ P2) \/ (P3 \/ P4));

        then

         A30: x in (P1 \/ P2) or x in (P3 \/ P4) by XBOOLE_0:def 3;

        per cases by A30, XBOOLE_0:def 3;

          suppose x in P1;

          then ex p st x = p & (p `2 ) < ( S-bound ( L~ f));

          hence thesis by A21, Th40;

        end;

          suppose x in P2;

          then ex p st x = p & (p `2 ) > ( N-bound ( L~ f));

          hence thesis by A28, Th40;

        end;

          suppose x in P3;

          then ex p st x = p & (p `1 ) > ( E-bound ( L~ f));

          hence thesis by A27, Th40;

        end;

          suppose x in P4;

          then ex p st x = p & (p `1 ) < ( W-bound ( L~ f));

          hence thesis by A2, Th40;

        end;

      end;

      for p st p in P1 holds (p `2 ) < ((( GoB f) * (1,1)) `2 )

      proof

        let p;

        assume p in P1;

        then ex q st p = q & (q `2 ) < ( S-bound ( L~ f));

        hence thesis by JORDAN5D: 38;

      end;

      then P1 misses ( L~ f) by GOBOARD8: 23;

      then (P1 \/ P2) misses ( L~ f) by A3, XBOOLE_1: 70;

      then ( LeftComp ( SpStSeq ( L~ f))) misses ( L~ f) by A29, A23, XBOOLE_1: 70;

      then

       A31: ( LeftComp ( SpStSeq ( L~ f))) c= (( L~ f) ` ) by SUBSET_1: 23;

      ( LeftComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1;

      hence thesis by A26, A20, A31, GOBOARD9: 4;

    end;

    begin

    theorem :: SPRECT_3:42

    

     Th42: for f be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2) holds <*p, q*> is_in_the_area_of f iff <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f

    proof

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

      thus <*p, q*> is_in_the_area_of f implies <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f

      proof

        

         A1: ( dom <*p, q*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

        then

         A2: 1 in ( dom <*p, q*>) by TARSKI:def 2;

        assume

         A3: <*p, q*> is_in_the_area_of f;

        

         A4: ( <*p, q*> /. 1) = p by FINSEQ_4: 17;

        then

         A5: (p `1 ) <= ( E-bound ( L~ f)) by A3, A2;

        

         A6: (p `2 ) <= ( N-bound ( L~ f)) by A3, A2, A4;

        

         A7: ( S-bound ( L~ f)) <= (p `2 ) by A3, A2, A4;

        

         A8: ( W-bound ( L~ f)) <= (p `1 ) by A3, A2, A4;

        thus <*p*> is_in_the_area_of f

        proof

          let i;

          assume i in ( dom <*p*>);

          then i in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

          then i = 1 by TARSKI:def 1;

          hence thesis by A8, A5, A7, A6, FINSEQ_4: 16;

        end;

        let i;

        assume i in ( dom <*q*>);

        then i in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

         A9: i = 1 by TARSKI:def 1;

        

         A10: ( <*p, q*> /. 2) = q by FINSEQ_4: 17;

        

         A11: 2 in ( dom <*p, q*>) by A1, TARSKI:def 2;

        then

         A12: (q `1 ) <= ( E-bound ( L~ f)) by A3, A10;

        

         A13: (q `2 ) <= ( N-bound ( L~ f)) by A3, A11, A10;

        

         A14: ( S-bound ( L~ f)) <= (q `2 ) by A3, A11, A10;

        ( W-bound ( L~ f)) <= (q `1 ) by A3, A11, A10;

        hence thesis by A12, A14, A13, A9, FINSEQ_4: 16;

      end;

      

       A15: ( <*p*> /. 1) = p by FINSEQ_4: 16;

      ( dom <*q*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      then

       A16: 1 in ( dom <*q*>) by TARSKI:def 1;

      ( dom <*p*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      then

       A17: 1 in ( dom <*p*>) by TARSKI:def 1;

      assume

       A18: <*p*> is_in_the_area_of f;

      then

       A19: (p `1 ) <= ( E-bound ( L~ f)) by A17, A15;

      

       A20: (p `2 ) <= ( N-bound ( L~ f)) by A18, A17, A15;

      

       A21: ( S-bound ( L~ f)) <= (p `2 ) by A18, A17, A15;

      

       A22: ( <*q*> /. 1) = q by FINSEQ_4: 16;

      assume

       A23: <*q*> is_in_the_area_of f;

      then

       A24: ( W-bound ( L~ f)) <= (q `1 ) by A16, A22;

      

       A25: (q `1 ) <= ( E-bound ( L~ f)) by A23, A16, A22;

      let i;

      assume i in ( dom <*p, q*>);

      then i in {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      then

       A26: i = 1 or i = 2 by TARSKI:def 2;

      

       A27: (q `2 ) <= ( N-bound ( L~ f)) by A23, A16, A22;

      

       A28: ( S-bound ( L~ f)) <= (q `2 ) by A23, A16, A22;

      ( W-bound ( L~ f)) <= (p `1 ) by A18, A17, A15;

      hence thesis by A19, A21, A20, A24, A25, A28, A27, A26, FINSEQ_4: 17;

    end;

    theorem :: SPRECT_3:43

    

     Th43: for f be rectangular FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st <*p*> is_in_the_area_of f & ((p `1 ) = ( W-bound ( L~ f)) or (p `1 ) = ( E-bound ( L~ f)) or (p `2 ) = ( S-bound ( L~ f)) or (p `2 ) = ( N-bound ( L~ f))) holds p in ( L~ f)

    proof

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

      

       A1: ( <*p*> /. 1) = p by FINSEQ_4: 16;

      ( dom <*p*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      then

       A2: 1 in ( dom <*p*>) by TARSKI:def 1;

      assume

       A3: <*p*> is_in_the_area_of f;

      then

       A4: ( W-bound ( L~ f)) <= (p `1 ) by A2, A1;

      

       A5: (p `2 ) <= ( N-bound ( L~ f)) by A3, A2, A1;

      

       A6: ( S-bound ( L~ f)) <= (p `2 ) by A3, A2, A1;

      

       A7: (p `1 ) <= ( E-bound ( L~ f)) by A3, A2, A1;

      consider D be non vertical non horizontal non empty compact Subset of ( TOP-REAL 2) such that

       A8: f = ( SpStSeq D) by SPRECT_1:def 2;

      

       A9: ( E-bound ( L~ ( SpStSeq D))) = ( E-bound D) by SPRECT_1: 61;

      

       A10: ( N-bound ( L~ ( SpStSeq D))) = ( N-bound D) by SPRECT_1: 60;

      

       A11: ( S-bound ( L~ ( SpStSeq D))) = ( S-bound D) by SPRECT_1: 59;

      

       A12: ( W-bound ( L~ ( SpStSeq D))) = ( W-bound D) by SPRECT_1: 58;

      

       A13: ( L~ f) = ((( LSeg (( NW-corner D),( NE-corner D))) \/ ( LSeg (( NE-corner D),( SE-corner D)))) \/ (( LSeg (( SE-corner D),( SW-corner D))) \/ ( LSeg (( SW-corner D),( NW-corner D))))) by A8, SPRECT_1: 41;

      assume

       A14: (p `1 ) = ( W-bound ( L~ f)) or (p `1 ) = ( E-bound ( L~ f)) or (p `2 ) = ( S-bound ( L~ f)) or (p `2 ) = ( N-bound ( L~ f));

      per cases by A14;

        suppose

         A15: (p `1 ) = ( W-bound ( L~ f));

        

         A16: (( NW-corner D) `1 ) = ( W-bound D) by EUCLID: 52;

        

         A17: (( NW-corner D) `2 ) = ( N-bound D) by EUCLID: 52;

        

         A18: (( SW-corner D) `2 ) = ( S-bound D) by EUCLID: 52;

        (( SW-corner D) `1 ) = ( W-bound D) by EUCLID: 52;

        then p in ( LSeg (( SW-corner D),( NW-corner D))) by A6, A5, A8, A12, A11, A10, A15, A16, A18, A17, GOBOARD7: 7;

        then p in (( LSeg (( SE-corner D),( SW-corner D))) \/ ( LSeg (( SW-corner D),( NW-corner D)))) by XBOOLE_0:def 3;

        hence thesis by A13, XBOOLE_0:def 3;

      end;

        suppose

         A19: (p `1 ) = ( E-bound ( L~ f));

        

         A20: (( SE-corner D) `1 ) = ( E-bound D) by EUCLID: 52;

        

         A21: (( SE-corner D) `2 ) = ( S-bound D) by EUCLID: 52;

        

         A22: (( NE-corner D) `2 ) = ( N-bound D) by EUCLID: 52;

        (( NE-corner D) `1 ) = ( E-bound D) by EUCLID: 52;

        then p in ( LSeg (( NE-corner D),( SE-corner D))) by A6, A5, A8, A11, A10, A9, A19, A20, A22, A21, GOBOARD7: 7;

        then p in (( LSeg (( NW-corner D),( NE-corner D))) \/ ( LSeg (( NE-corner D),( SE-corner D)))) by XBOOLE_0:def 3;

        hence thesis by A13, XBOOLE_0:def 3;

      end;

        suppose

         A23: (p `2 ) = ( S-bound ( L~ f));

        

         A24: (( SW-corner D) `1 ) = ( W-bound D) by EUCLID: 52;

        

         A25: (( SW-corner D) `2 ) = ( S-bound D) by EUCLID: 52;

        

         A26: (( SE-corner D) `2 ) = ( S-bound D) by EUCLID: 52;

        (( SE-corner D) `1 ) = ( E-bound D) by EUCLID: 52;

        then p in ( LSeg (( SE-corner D),( SW-corner D))) by A4, A7, A8, A12, A11, A9, A23, A24, A26, A25, GOBOARD7: 8;

        then p in (( LSeg (( SE-corner D),( SW-corner D))) \/ ( LSeg (( SW-corner D),( NW-corner D)))) by XBOOLE_0:def 3;

        hence thesis by A13, XBOOLE_0:def 3;

      end;

        suppose

         A27: (p `2 ) = ( N-bound ( L~ f));

        

         A28: (( NE-corner D) `1 ) = ( E-bound D) by EUCLID: 52;

        

         A29: (( NE-corner D) `2 ) = ( N-bound D) by EUCLID: 52;

        

         A30: (( NW-corner D) `2 ) = ( N-bound D) by EUCLID: 52;

        (( NW-corner D) `1 ) = ( W-bound D) by EUCLID: 52;

        then p in ( LSeg (( NW-corner D),( NE-corner D))) by A4, A7, A8, A12, A10, A9, A27, A28, A30, A29, GOBOARD7: 8;

        then p in (( LSeg (( NW-corner D),( NE-corner D))) \/ ( LSeg (( NE-corner D),( SE-corner D)))) by XBOOLE_0:def 3;

        hence thesis by A13, XBOOLE_0:def 3;

      end;

    end;

    theorem :: SPRECT_3:44

    

     Th44: for f be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2), r be Real st 0 <= r & r <= 1 & <*p, q*> is_in_the_area_of f holds <*(((1 - r) * p) + (r * q))*> is_in_the_area_of f

    proof

      let f be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2), r be Real such that

       A1: 0 <= r and

       A2: r <= 1 and

       A3: <*p, q*> is_in_the_area_of f;

      

       A4: ( dom <*p, q*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      then

       A5: 2 in ( dom <*p, q*>) by TARSKI:def 2;

      

       A6: ( <*p, q*> /. 2) = q by FINSEQ_4: 17;

      then ( W-bound ( L~ f)) <= (q `1 ) by A3, A5;

      then

       A7: (r * ( W-bound ( L~ f))) <= (r * (q `1 )) by A1, XREAL_1: 64;

      (q `1 ) <= ( E-bound ( L~ f)) by A3, A5, A6;

      then

       A8: (r * (q `1 )) <= (r * ( E-bound ( L~ f))) by A1, XREAL_1: 64;

      

       A9: ( <*p, q*> /. 1) = p by FINSEQ_4: 17;

      

       A10: (1 - r) >= 0 by A2, XREAL_1: 48;

      

       A11: 1 in ( dom <*p, q*>) by A4, TARSKI:def 2;

      then ( W-bound ( L~ f)) <= (p `1 ) by A3, A9;

      then

       A12: ((1 - r) * ( W-bound ( L~ f))) <= ((1 - r) * (p `1 )) by A10, XREAL_1: 64;

      (p `1 ) <= ( E-bound ( L~ f)) by A3, A11, A9;

      then

       A13: ((1 - r) * (p `1 )) <= ((1 - r) * ( E-bound ( L~ f))) by A10, XREAL_1: 64;

      ( S-bound ( L~ f)) <= (p `2 ) by A3, A11, A9;

      then

       A14: ((1 - r) * ( S-bound ( L~ f))) <= ((1 - r) * (p `2 )) by A10, XREAL_1: 64;

      

       A15: ((((1 - r) * p) + (r * q)) `1 ) = ((((1 - r) * p) `1 ) + ((r * q) `1 )) by TOPREAL3: 2

      .= (((1 - r) * (p `1 )) + ((r * q) `1 )) by TOPREAL3: 4

      .= (((1 - r) * (p `1 )) + (r * (q `1 ))) by TOPREAL3: 4;

      (p `2 ) <= ( N-bound ( L~ f)) by A3, A11, A9;

      then

       A16: ((1 - r) * (p `2 )) <= ((1 - r) * ( N-bound ( L~ f))) by A10, XREAL_1: 64;

      let n;

      

       A17: ( dom <*(((1 - r) * p) + (r * q))*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      assume n in ( dom <*(((1 - r) * p) + (r * q))*>);

      then

       A18: n = 1 by A17, TARSKI:def 1;

      (((1 - r) * ( W-bound ( L~ f))) + (r * ( W-bound ( L~ f)))) = (1 * ( W-bound ( L~ f)));

      then ( W-bound ( L~ f)) <= (((1 - r) * (p `1 )) + (r * (q `1 ))) by A7, A12, XREAL_1: 7;

      hence ( W-bound ( L~ f)) <= (( <*(((1 - r) * p) + (r * q))*> /. n) `1 ) by A18, A15, FINSEQ_4: 16;

      (((1 - r) * ( E-bound ( L~ f))) + (r * ( E-bound ( L~ f)))) = (1 * ( E-bound ( L~ f)));

      then (((1 - r) * (p `1 )) + (r * (q `1 ))) <= ( E-bound ( L~ f)) by A8, A13, XREAL_1: 7;

      hence (( <*(((1 - r) * p) + (r * q))*> /. n) `1 ) <= ( E-bound ( L~ f)) by A18, A15, FINSEQ_4: 16;

      

       A19: ((((1 - r) * p) + (r * q)) `2 ) = ((((1 - r) * p) `2 ) + ((r * q) `2 )) by TOPREAL3: 2

      .= (((1 - r) * (p `2 )) + ((r * q) `2 )) by TOPREAL3: 4

      .= (((1 - r) * (p `2 )) + (r * (q `2 ))) by TOPREAL3: 4;

      (q `2 ) <= ( N-bound ( L~ f)) by A3, A5, A6;

      then

       A20: (r * (q `2 )) <= (r * ( N-bound ( L~ f))) by A1, XREAL_1: 64;

      ( S-bound ( L~ f)) <= (q `2 ) by A3, A5, A6;

      then

       A21: (r * ( S-bound ( L~ f))) <= (r * (q `2 )) by A1, XREAL_1: 64;

      (((1 - r) * ( S-bound ( L~ f))) + (r * ( S-bound ( L~ f)))) = (1 * ( S-bound ( L~ f)));

      then ( S-bound ( L~ f)) <= (((1 - r) * (p `2 )) + (r * (q `2 ))) by A21, A14, XREAL_1: 7;

      hence ( S-bound ( L~ f)) <= (( <*(((1 - r) * p) + (r * q))*> /. n) `2 ) by A18, A19, FINSEQ_4: 16;

      (((1 - r) * ( N-bound ( L~ f))) + (r * ( N-bound ( L~ f)))) = (1 * ( N-bound ( L~ f)));

      then (((1 - r) * (p `2 )) + (r * (q `2 ))) <= ( N-bound ( L~ f)) by A20, A16, XREAL_1: 7;

      hence thesis by A18, A19, FINSEQ_4: 16;

    end;

    theorem :: SPRECT_3:45

    

     Th45: for f,g be FinSequence of ( TOP-REAL 2) st g is_in_the_area_of f & i in ( dom g) holds <*(g /. i)*> is_in_the_area_of f

    proof

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

       A1: g is_in_the_area_of f and

       A2: i in ( dom g);

      let n;

      

       A3: ( dom <*(g /. i)*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      assume n in ( dom <*(g /. i)*>);

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

      then ( <*(g /. i)*> /. n) = (g /. i) by FINSEQ_4: 16;

      hence thesis by A1, A2;

    end;

    theorem :: SPRECT_3:46

    

     Th46: for f,g be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st g is_in_the_area_of f & p in ( L~ g) holds <*p*> is_in_the_area_of f

    proof

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

       A1: g is_in_the_area_of f;

      assume p in ( L~ g);

      then

      consider i such that

       A2: 1 <= i and

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

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

      

       A5: ex r be Real st p = (((1 - r) * (g /. i)) + (r * (g /. (i + 1)))) & 0 <= r & r <= 1 by A4;

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

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

      then i in ( dom g) by A2, FINSEQ_3: 25;

      then

       A6: <*(g /. i)*> is_in_the_area_of f by A1, Th45;

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

      then (i + 1) in ( dom g) by A3, FINSEQ_3: 25;

      then <*(g /. (i + 1))*> is_in_the_area_of f by A1, Th45;

      then <*(g /. i), (g /. (i + 1))*> is_in_the_area_of f by A6, Th42;

      hence thesis by A5, Th44;

    end;

    theorem :: SPRECT_3:47

    

     Th47: for f be rectangular FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2) st not q in ( L~ f) & <*p, q*> is_in_the_area_of f holds (( LSeg (p,q)) /\ ( L~ f)) c= {p}

    proof

      let f be rectangular FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2) such that

       A1: not q in ( L~ f);

      assume

       A2: <*p, q*> is_in_the_area_of f;

      

       A3: ( dom <*p, q*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      then

       A4: 2 in ( dom <*p, q*>) by TARSKI:def 2;

      

       A5: ( <*p, q*> /. 2) = q by FINSEQ_4: 17;

      then

       A6: ( W-bound ( L~ f)) <= (q `1 ) by A2, A4;

      

       A7: <*q*> is_in_the_area_of f by A2, Th42;

      then (q `1 ) <> ( W-bound ( L~ f)) by A1, Th43;

      then

       A8: ( W-bound ( L~ f)) < (q `1 ) by A6, XXREAL_0: 1;

      

       A9: (q `2 ) <= ( N-bound ( L~ f)) by A2, A4, A5;

      (q `2 ) <> ( N-bound ( L~ f)) by A1, A7, Th43;

      then

       A10: (q `2 ) < ( N-bound ( L~ f)) by A9, XXREAL_0: 1;

      let x be object;

      

       A11: ( <*p, q*> /. 1) = p by FINSEQ_4: 17;

      

       A12: (q `1 ) <= ( E-bound ( L~ f)) by A2, A4, A5;

      (q `1 ) <> ( E-bound ( L~ f)) by A1, A7, Th43;

      then

       A13: (q `1 ) < ( E-bound ( L~ f)) by A12, XXREAL_0: 1;

      assume

       A14: x in (( LSeg (p,q)) /\ ( L~ f));

      then

      reconsider p9 = x as Point of ( TOP-REAL 2);

      

       A15: p9 in ( L~ f) by A14, XBOOLE_0:def 4;

      

       A16: 1 in ( dom <*p, q*>) by A3, TARSKI:def 2;

      then

       A17: ( W-bound ( L~ f)) <= (p `1 ) by A2, A11;

      

       A18: (p `2 ) <= ( N-bound ( L~ f)) by A2, A16, A11;

      

       A19: ( S-bound ( L~ f)) <= (p `2 ) by A2, A16, A11;

      

       A20: (p `1 ) <= ( E-bound ( L~ f)) by A2, A16, A11;

      

       A21: ( S-bound ( L~ f)) <= (q `2 ) by A2, A4, A5;

      (q `2 ) <> ( S-bound ( L~ f)) by A1, A7, Th43;

      then

       A22: ( S-bound ( L~ f)) < (q `2 ) by A21, XXREAL_0: 1;

      x in ( LSeg (p,q)) by A14, XBOOLE_0:def 4;

      then

      consider r be Real such that

       A23: p9 = (((1 - r) * p) + (r * q)) and

       A24: 0 <= r and

       A25: r <= 1;

      

       A26: (p9 `1 ) = ((((1 - r) * p) `1 ) + ((r * q) `1 )) by A23, TOPREAL3: 2

      .= (((1 - r) * (p `1 )) + ((r * q) `1 )) by TOPREAL3: 4

      .= (((1 - r) * (p `1 )) + (r * (q `1 ))) by TOPREAL3: 4;

      

       A27: (p9 `2 ) = ((((1 - r) * p) `2 ) + ((r * q) `2 )) by A23, TOPREAL3: 2

      .= (((1 - r) * (p `2 )) + ((r * q) `2 )) by TOPREAL3: 4

      .= (((1 - r) * (p `2 )) + (r * (q `2 ))) by TOPREAL3: 4;

      per cases by A15, Th32;

        suppose (p9 `1 ) = ( W-bound ( L~ f));

        then r = 0 by A17, A8, A24, A25, A26, XREAL_1: 180;

        

        then p9 = ((1 * p) + ( 0. ( TOP-REAL 2))) by A23, RLVECT_1: 10

        .= (1 * p) by RLVECT_1: 4

        .= p by RLVECT_1:def 8;

        hence thesis by ZFMISC_1: 31;

      end;

        suppose (p9 `1 ) = ( E-bound ( L~ f));

        then r = 0 by A20, A13, A24, A25, A26, XREAL_1: 179;

        

        then p9 = ((1 * p) + ( 0. ( TOP-REAL 2))) by A23, RLVECT_1: 10

        .= (1 * p) by RLVECT_1: 4

        .= p by RLVECT_1:def 8;

        hence thesis by ZFMISC_1: 31;

      end;

        suppose (p9 `2 ) = ( S-bound ( L~ f));

        then r = 0 by A19, A22, A24, A25, A27, XREAL_1: 180;

        

        then p9 = ((1 * p) + ( 0. ( TOP-REAL 2))) by A23, RLVECT_1: 10

        .= (1 * p) by RLVECT_1: 4

        .= p by RLVECT_1:def 8;

        hence thesis by ZFMISC_1: 31;

      end;

        suppose (p9 `2 ) = ( N-bound ( L~ f));

        then r = 0 by A18, A10, A24, A25, A27, XREAL_1: 179;

        

        then p9 = ((1 * p) + ( 0. ( TOP-REAL 2))) by A23, RLVECT_1: 10

        .= (1 * p) by RLVECT_1: 4

        .= p by RLVECT_1:def 8;

        hence thesis by ZFMISC_1: 31;

      end;

    end;

    theorem :: SPRECT_3:48

    for f be rectangular FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2) st p in ( L~ f) & not q in ( L~ f) & <*q*> is_in_the_area_of f holds (( LSeg (p,q)) /\ ( L~ f)) = {p}

    proof

      let f be rectangular FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2) such that

       A1: p in ( L~ f) and

       A2: not q in ( L~ f) and

       A3: <*q*> is_in_the_area_of f;

      

       A4: <*p, q*> = ( <*p*> ^ <*q*>) by FINSEQ_1:def 9;

       <*p*> is_in_the_area_of f by A1, Th46, SPRECT_2: 21;

      hence (( LSeg (p,q)) /\ ( L~ f)) c= {p} by A2, A3, A4, Th47, SPRECT_2: 24;

      p in ( LSeg (p,q)) by RLTOPSP1: 68;

      then p in (( LSeg (p,q)) /\ ( L~ f)) by A1, XBOOLE_0:def 4;

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: SPRECT_3:49

    

     Th49: for f be non constant standard special_circular_sequence st 1 <= i & i <= ( len ( GoB f)) & 1 <= j & j <= ( width ( GoB f)) holds <*(( GoB f) * (i,j))*> is_in_the_area_of f

    proof

      let f be non constant standard special_circular_sequence such that

       A1: 1 <= i and

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

       A3: 1 <= j and

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

      set G = ( GoB f);

      

       A5: 1 <= ( width G) by A3, A4, XXREAL_0: 2;

      

       A6: 1 <= ( len G) by A1, A2, XXREAL_0: 2;

      

       A7: ( N-bound ( L~ f)) = ((G * (1,( width G))) `2 ) by JORDAN5D: 40

      .= ((G * (i,( width G))) `2 ) by A1, A2, A5, GOBOARD5: 1;

      

       A8: j = 1 or j > 1 by A3, XXREAL_0: 1;

      

       A9: ( S-bound ( L~ f)) = ((G * (1,1)) `2 ) by JORDAN5D: 38

      .= ((G * (i,1)) `2 ) by A1, A2, A5, GOBOARD5: 1;

      

       A10: i = 1 or i > 1 by A1, XXREAL_0: 1;

      

       A11: ( E-bound ( L~ f)) = ((G * (( len G),1)) `1 ) by JORDAN5D: 39

      .= ((G * (( len G),j)) `1 ) by A3, A4, A6, GOBOARD5: 2;

      

       A12: j = ( width G) or j < ( width G) by A4, XXREAL_0: 1;

      

       A13: i = ( len G) or i < ( len G) by A2, XXREAL_0: 1;

      let n;

      set p = (( GoB f) * (i,j));

      assume n in ( dom <*(( GoB f) * (i,j))*>);

      then n in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      then n = 1 by TARSKI:def 1;

      then

       A14: ( <*p*> /. n) = p by FINSEQ_4: 16;

      ( W-bound ( L~ f)) = ((G * (1,1)) `1 ) by JORDAN5D: 37

      .= ((G * (1,j)) `1 ) by A3, A4, A6, GOBOARD5: 2;

      hence thesis by A14, A10, A9, A8, A11, A13, A7, A12, GOBOARD5: 3, GOBOARD5: 4;

    end;

    theorem :: SPRECT_3:50

    for g be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2) st <*p, q*> is_in_the_area_of g holds <*((1 / 2) * (p + q))*> is_in_the_area_of g

    proof

      let g be FinSequence of ( TOP-REAL 2), p,q be Point of ( TOP-REAL 2);

      ((1 / 2) * (p + q)) = (((1 - (1 / 2)) * p) + ((1 / 2) * q)) by RLVECT_1:def 5;

      hence thesis by Th44;

    end;

    theorem :: SPRECT_3:51

    for f,g be FinSequence of ( TOP-REAL 2) st g is_in_the_area_of f holds ( Rev g) is_in_the_area_of f

    proof

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

       A1: g is_in_the_area_of f;

      

       A2: ( Rev ( Rev g)) = g;

      let n such that

       A3: n in ( dom ( Rev g));

      n >= 1 by A3, FINSEQ_3: 25;

      then

       A4: (n - 1) >= 0 by XREAL_1: 48;

      set i = ((( len g) + 1) -' n);

      

       A5: ( len ( Rev g)) = ( len g) by FINSEQ_5:def 3;

      then

       A6: n <= ( len g) by A3, FINSEQ_3: 25;

      then

       A7: i = ((( len g) -' n) + 1) by NAT_D: 38;

      

      then i = ((( len g) - n) + 1) by A6, XREAL_1: 233

      .= (( len g) - (n - 1));

      then

       A8: i <= (( len g) - 0 ) by A4, XREAL_1: 13;

      1 <= i by A7, NAT_1: 11;

      then

       A9: i in ( dom g) by A8, FINSEQ_3: 25;

      ( len g) <= (( len g) + 1) by NAT_1: 11;

      then (n + i) = (( len g) + 1) by A6, XREAL_1: 235, XXREAL_0: 2;

      then (( Rev g) /. n) = (g /. i) by A2, A5, A3, FINSEQ_5: 66;

      hence thesis by A1, A9;

    end;

    theorem :: SPRECT_3:52

    for f,g be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in ( L~ g) holds ( R_Cut (g,p)) is_in_the_area_of f

    proof

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

       A1: g is_in_the_area_of f and

       A2: <*p*> is_in_the_area_of f and

       A3: g is being_S-Seq;

      2 <= ( len g) by A3, TOPREAL1:def 8;

      then 1 <= ( len g) by XXREAL_0: 2;

      then

       A5: 1 in ( dom g) by FINSEQ_3: 25;

      assume

       A6: p in ( L~ g);

      then

       A7: ( Index (p,g)) < ( len g) by JORDAN3: 8;

      1 <= ( Index (p,g)) by A6, JORDAN3: 8;

      then

       A8: ( Index (p,g)) in ( dom g) by A7, FINSEQ_3: 25;

      per cases ;

        suppose p <> (g . 1);

        then

         A9: ( R_Cut (g,p)) = (( mid (g,1,( Index (p,g)))) ^ <*p*>) by JORDAN3:def 4;

        ( mid (g,1,( Index (p,g)))) is_in_the_area_of f by A1, A5, A8, SPRECT_2: 22;

        hence thesis by A2, A9, SPRECT_2: 24;

      end;

        suppose p = (g . 1);

        

        then ( R_Cut (g,p)) = <*(g . 1)*> by JORDAN3:def 4

        .= ( mid (g,1,1)) by A5, JORDAN4: 15;

        hence thesis by A1, A5, SPRECT_2: 22;

      end;

    end;

    theorem :: SPRECT_3:53

    for f be non constant standard special_circular_sequence, g be FinSequence of ( TOP-REAL 2) holds g is_in_the_area_of f iff g is_in_the_area_of ( SpStSeq ( L~ f))

    proof

      let f be non constant standard special_circular_sequence, g be FinSequence of ( TOP-REAL 2);

      

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

      

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

      

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

      

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

      thus g is_in_the_area_of f implies g is_in_the_area_of ( SpStSeq ( L~ f)) by A4, A1, A2, A3;

      assume

       A5: g is_in_the_area_of ( SpStSeq ( L~ f));

      let n;

      thus thesis by A4, A1, A2, A3, A5;

    end;

    theorem :: SPRECT_3:54

    for f be rectangular special_circular_sequence, g be S-Sequence_in_R2 st (g /. 1) in ( LeftComp f) & (g /. ( len g)) in ( RightComp f) holds ( L_Cut (g,( Last_Point (( L~ g),(g /. 1),(g /. ( len g)),( L~ f))))) is_in_the_area_of f

    proof

      let f be rectangular special_circular_sequence, g be S-Sequence_in_R2 such that

       A1: (g /. 1) in ( LeftComp f) and

       A2: (g /. ( len g)) in ( RightComp f);

      

       A3: ( L~ g) meets ( L~ f) by A1, A2, Th33;

      1 in ( dom g) by FINSEQ_5: 6;

      then

       A4: ( len g) >= 1 by FINSEQ_3: 25;

      set lp = ( Last_Point (( L~ g),(g /. 1),(g /. ( len g)),( L~ f))), ilp = ( Index (lp,g)), h = ( L_Cut (g,lp));

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

      then

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

      then

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

      then

       A7: 1 <= ilp by JORDAN3: 8;

      

       A8: lp in ( LSeg (g,ilp)) by A6, JORDAN3: 9;

      

       A9: ilp < ( len g) by A6, JORDAN3: 8;

      then

       A10: (ilp + 1) <= ( len g) by NAT_1: 13;

      given n such that

       A11: n in ( dom h) and

       A12: ( W-bound ( L~ f)) > ((h /. n) `1 ) or ((h /. n) `1 ) > ( E-bound ( L~ f)) or ( S-bound ( L~ f)) > ((h /. n) `2 ) or ((h /. n) `2 ) > ( N-bound ( L~ f));

      

       A13: 1 <= n by A11, FINSEQ_3: 25;

      then

       A14: ((ilp + n) -' 1) = (ilp + (n -' 1)) by NAT_D: 38;

      ( LeftComp f) = { p : not (( W-bound ( L~ f)) <= (p `1 ) & (p `1 ) <= ( E-bound ( L~ f)) & ( S-bound ( L~ f)) <= (p `2 ) & (p `2 ) <= ( N-bound ( L~ f))) } by Th37;

      then

       A15: (h /. n) in ( LeftComp f) by A12;

      

       A16: 1 <= (ilp + 1) by NAT_1: 11;

      then

       A17: (ilp + 1) in ( dom g) by A10, FINSEQ_3: 25;

      

       A18: ( LeftComp f) misses ( RightComp f) by SPRECT_1: 88;

      

       A19: ( L~ f) misses ( LeftComp f) by Th26;

      

       A20: ( len g) in ( dom g) by FINSEQ_5: 6;

      

       A21: lp in ( L~ f) by A5, XBOOLE_0:def 4;

      now

        assume

         A22: n = 1;

        per cases ;

          suppose lp <> (g . (ilp + 1));

          then h = ( <*lp*> ^ ( mid (g,(ilp + 1),( len g)))) by JORDAN3:def 3;

          then (h /. n) = lp by A22, FINSEQ_5: 15;

          hence contradiction by A19, A21, A15, XBOOLE_0: 3;

        end;

          suppose

           A23: lp = (g . (ilp + 1));

          then h = ( mid (g,(ilp + 1),( len g))) by JORDAN3:def 3;

          

          then (h /. n) = (g /. ((1 + (ilp + 1)) -' 1)) by A20, A11, A10, A17, A22, SPRECT_2: 3

          .= (g /. (ilp + 1)) by NAT_D: 34

          .= lp by A17, A23, PARTFUN1:def 6;

          hence contradiction by A19, A21, A15, XBOOLE_0: 3;

        end;

      end;

      then

       A24: n > 1 by A13, XXREAL_0: 1;

      then

       A25: (1 + 1) < (ilp + n) by A7, XREAL_1: 8;

      then

       A26: 1 <= ((ilp + n) -' 1) by NAT_D: 49;

      set m = ( mid (g,(ilp + n),( len g)));

      

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

      

       A28: n <= ( len h) by A11, FINSEQ_3: 25;

      then

       A29: (n + ilp) <= (( len h) + ilp) by XREAL_1: 6;

      

       A30: n = ((n -' 1) + 1) by A13, XREAL_1: 235;

      then

       A31: 1 <= (n -' 1) by A24, NAT_1: 13;

      

       A32: ( len ( mid (g,(ilp + 1),( len g)))) = ((( len g) -' (ilp + 1)) + 1) by A10, A16, JORDAN4: 8

      .= (( len g) -' ilp) by A6, JORDAN3: 8, NAT_2: 7;

      then

       A33: ((ilp + ( len ( mid (g,(ilp + 1),( len g))))) + 1) = (( len g) + 1) by A9, XREAL_1: 235;

      now

        

         A34: (ilp + 1) <= ((ilp + n) -' 1) by A14, A31, XREAL_1: 6;

        assume

         A35: lp <> (g . (ilp + 1));

        then

         A36: h = ( <*lp*> ^ ( mid (g,(ilp + 1),( len g)))) by JORDAN3:def 3;

        then

         A37: ( len h) = (1 + ( len ( mid (g,(ilp + 1),( len g))))) by A27, FINSEQ_1: 22;

        then

         A38: ((ilp + n) -' 1) <= ( len g) by A33, A29, NAT_D: 53;

        

         A39: (( len h) -' 1) = ( len ( mid (g,(ilp + 1),( len g)))) by A37, NAT_D: 34;

        then (n -' 1) <= ( len ( mid (g,(ilp + 1),( len g)))) by A28, NAT_D: 42;

        then

         A40: (n -' 1) in ( dom ( mid (g,(ilp + 1),( len g)))) by A31, FINSEQ_3: 25;

        (h /. n) = (( mid (g,(ilp + 1),( len g))) /. (n -' 1)) by A28, A30, A27, A31, A36, A39, NAT_D: 42, SEQ_4: 136;

        

        then

         A41: (h /. n) = (g /. (((n -' 1) + (ilp + 1)) -' 1)) by A20, A10, A17, A40, SPRECT_2: 3

        .= (g /. ((n + ilp) -' 1)) by A30;

        then

         A42: ((ilp + n) -' 1) <> ( len g) by A2, A15, A18, XBOOLE_0: 3;

        then

         A43: ((ilp + n) -' 1) < ( len g) by A38, XXREAL_0: 1;

        reconsider m = ( mid (g,((ilp + n) -' 1),( len g))) as S-Sequence_in_R2 by A4, A26, A38, A42, JORDAN3: 6;

        

         A44: ((ilp + n) -' 1) in ( dom g) by A26, A38, FINSEQ_3: 25;

        then

         A45: (m /. ( len m)) in ( RightComp f) by A2, A20, SPRECT_2: 9;

        (m /. 1) in ( LeftComp f) by A20, A15, A41, A44, SPRECT_2: 8;

        then ( L~ f) meets ( L~ m) by A45, Th33;

        then

        consider q be object such that

         A46: q in ( L~ f) and

         A47: q in ( L~ m) by XBOOLE_0: 3;

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

        consider i such that

         A48: 1 <= i and

         A49: (i + 1) <= ( len m) and

         A50: q in ( LSeg (m,i)) by A47, SPPOL_2: 13;

        

         A51: ( len m) = ((( len g) -' ((ilp + n) -' 1)) + 1) by A26, A38, JORDAN4: 8;

        then i <= (( len g) -' ((ilp + n) -' 1)) by A49, XREAL_1: 6;

        then

         A52: (i + ((ilp + n) -' 1)) <= ( len g) by A38, NAT_D: 54;

        i < ( len m) by A49, NAT_1: 13;

        then

         A53: ( LSeg (m,i)) = ( LSeg (g,((i + ((ilp + n) -' 1)) -' 1))) by A26, A48, A51, A43, JORDAN4: 19;

        set j = ((i + ((ilp + n) -' 1)) -' 1);

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

        then

         A54: (j + 1) <= ( len g) by A48, A52, XREAL_1: 235, XXREAL_0: 2;

        j = ((i -' 1) + ((ilp + n) -' 1)) by A48, NAT_D: 38;

        then j >= ((ilp + n) -' 1) by NAT_1: 11;

        then

         A55: (ilp + 1) <= j by A34, XXREAL_0: 2;

        

         A56: lp <> (g /. (ilp + 1)) by A17, A35, PARTFUN1:def 6;

         A57:

        now

          assume lp = q;

          then

           A58: lp in (( LSeg (g,ilp)) /\ ( LSeg (g,j))) by A8, A50, A53, XBOOLE_0:def 4;

          then

           A59: ( LSeg (g,ilp)) meets ( LSeg (g,j));

          per cases by A55, XXREAL_0: 1;

            suppose

             A60: (ilp + 1) = j;

            then (ilp + (1 + 1)) <= ( len g) by A54;

            then (( LSeg (g,ilp)) /\ ( LSeg (g,(ilp + 1)))) = {(g /. (ilp + 1))} by A7, TOPREAL1:def 6;

            hence contradiction by A56, A58, A60, TARSKI:def 1;

          end;

            suppose (ilp + 1) < j;

            hence contradiction by A59, TOPREAL1:def 7;

          end;

        end;

        1 <= j by A16, A55, XXREAL_0: 2;

        then ilp >= j by A3, A8, A10, A7, A46, A50, A53, A54, A57, JORDAN5C: 28;

        then ilp >= (ilp + 1) by A55, XXREAL_0: 2;

        hence contradiction by XREAL_1: 29;

      end;

      then

       A61: h = ( mid (g,(ilp + 1),( len g))) by JORDAN3:def 3;

      then

       A62: (ilp + ( len h)) = ( len g) by A9, A32, XREAL_1: 235;

      then

       A63: m = (g /^ ((ilp + n) -' 1)) by A29, FINSEQ_6: 117;

      

       A64: 1 <= (ilp + n) by A25, XXREAL_0: 2;

      (((ilp + n) -' 1) + 1) = (ilp + n) by A25, XREAL_1: 235, XXREAL_0: 2;

      then ((ilp + n) -' 1) < ( len g) by A29, A62, NAT_1: 13;

      then

       A65: (m /. ( len m)) in ( RightComp f) by A2, A63, JORDAN4: 6;

      

       A66: (h /. n) = (g /. ((n + (ilp + 1)) -' 1)) by A20, A11, A10, A17, A61, SPRECT_2: 3

      .= (g /. (((n + ilp) + 1) -' 1))

      .= (g /. (ilp + n)) by NAT_D: 34;

      then

       A67: (ilp + n) <> ( len g) by A2, A15, A18, XBOOLE_0: 3;

      then

      reconsider m as S-Sequence_in_R2 by A4, A29, A62, A64, JORDAN3: 6;

      (ilp + n) in ( dom g) by A29, A62, A64, FINSEQ_3: 25;

      then (m /. 1) in ( LeftComp f) by A20, A15, A66, SPRECT_2: 8;

      then ( L~ f) meets ( L~ m) by A65, Th33;

      then

      consider q be object such that

       A68: q in ( L~ f) and

       A69: q in ( L~ m) by XBOOLE_0: 3;

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

      consider i such that

       A70: 1 <= i and

       A71: (i + 1) <= ( len m) and

       A72: q in ( LSeg (m,i)) by A69, SPPOL_2: 13;

      set j = ((i + (ilp + n)) -' 1);

      

       A73: j = ((i -' 1) + (ilp + n)) by A70, NAT_D: 38;

      then

       A74: j >= (ilp + n) by NAT_1: 11;

      ( len m) = ((( len g) -' (ilp + n)) + 1) by A4, A29, A62, A64, FINSEQ_6: 118;

      then

       A75: i < ((( len g) -' (ilp + n)) + 1) by A71, NAT_1: 13;

      then (i -' 1) < (( len g) -' (ilp + n)) by A70, NAT_D: 54;

      then ((i -' 1) + (ilp + n)) < ( len g) by NAT_D: 53;

      then

       A76: (j + 1) <= ( len g) by A73, NAT_1: 13;

      (ilp + n) < ( len g) by A29, A62, A67, XXREAL_0: 1;

      then

       A77: ( LSeg (m,i)) = ( LSeg (g,((i + (ilp + n)) -' 1))) by A64, A70, A75, JORDAN4: 19;

      (ilp + 1) < (ilp + n) by A24, XREAL_1: 6;

      then

       A78: j > (ilp + 1) by A74, XXREAL_0: 2;

       A79:

      now

        assume lp = q;

        then lp in (( LSeg (g,ilp)) /\ ( LSeg (g,j))) by A8, A72, A77, XBOOLE_0:def 4;

        then ( LSeg (g,ilp)) meets ( LSeg (g,j));

        hence contradiction by A78, TOPREAL1:def 7;

      end;

      1 <= j by A64, A74, XXREAL_0: 2;

      then ilp >= j by A3, A8, A10, A7, A68, A72, A77, A79, A76, JORDAN5C: 28;

      then ilp >= (ilp + 1) by A78, XXREAL_0: 2;

      hence contradiction by XREAL_1: 29;

    end;

    theorem :: SPRECT_3:55

    for f be non constant standard special_circular_sequence st 1 <= i & i < ( len ( GoB f)) & 1 <= j & j < ( width ( GoB f)) holds ( Int ( cell (( GoB f),i,j))) misses ( L~ ( SpStSeq ( L~ f)))

    proof

      let f be non constant standard special_circular_sequence such that

       A1: 1 <= i and

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

       A3: 1 <= j and

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

      

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

      set G = ( GoB f);

      

       A6: ( Int ( cell (G,i,j))) = { |[r, s]| where r,s be Real : ((G * (i,1)) `1 ) < r & r < ((G * ((i + 1),1)) `1 ) & ((G * (1,j)) `2 ) < s & s < ((G * (1,(j + 1))) `2 ) } by A1, A2, A3, A4, GOBOARD6: 26;

      

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

      

       A8: 1 <= ( width ( GoB f)) by GOBRD11: 34;

      then

       A9: <*(( GoB f) * (i,1))*> is_in_the_area_of f by A1, A2, Th49;

      1 <= (i + 1) by A1, NAT_1: 13;

      then

       A10: <*(( GoB f) * ((i + 1),1))*> is_in_the_area_of f by A8, A5, Th49;

      assume ( Int ( cell (( GoB f),i,j))) meets ( L~ ( SpStSeq ( L~ f)));

      then

      consider x be object such that

       A11: x in ( Int ( cell (( GoB f),i,j))) and

       A12: x in ( L~ ( SpStSeq ( L~ f))) by XBOOLE_0: 3;

      

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

      

       A14: 1 <= ( len ( GoB f)) by GOBRD11: 34;

      then

       A15: <*(( GoB f) * (1,j))*> is_in_the_area_of f by A3, A4, Th49;

      

       A16: (j + 1) <= ( width ( GoB f)) by A4, NAT_1: 13;

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

      then

       A17: <*(( GoB f) * (1,(j + 1)))*> is_in_the_area_of f by A14, A16, Th49;

      

       A18: ( L~ ( SpStSeq ( L~ f))) = { p : (p `1 ) = ( W-bound ( L~ ( SpStSeq ( L~ f)))) & (p `2 ) <= ( N-bound ( L~ ( SpStSeq ( L~ f)))) & (p `2 ) >= ( S-bound ( L~ ( SpStSeq ( L~ f)))) or (p `1 ) <= ( E-bound ( L~ ( SpStSeq ( L~ f)))) & (p `1 ) >= ( W-bound ( L~ ( SpStSeq ( L~ f)))) & (p `2 ) = ( N-bound ( L~ ( SpStSeq ( L~ f)))) or (p `1 ) <= ( E-bound ( L~ ( SpStSeq ( L~ f)))) & (p `1 ) >= ( W-bound ( L~ ( SpStSeq ( L~ f)))) & (p `2 ) = ( S-bound ( L~ ( SpStSeq ( L~ f)))) or (p `1 ) = ( E-bound ( L~ ( SpStSeq ( L~ f)))) & (p `2 ) <= ( N-bound ( L~ ( SpStSeq ( L~ f)))) & (p `2 ) >= ( S-bound ( L~ ( SpStSeq ( L~ f)))) } by Th35;

      

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

      consider p such that

       A20: p = x and

       A21: (p `1 ) = ( W-bound ( L~ ( SpStSeq ( L~ f)))) & (p `2 ) <= ( N-bound ( L~ ( SpStSeq ( L~ f)))) & (p `2 ) >= ( S-bound ( L~ ( SpStSeq ( L~ f)))) or (p `1 ) <= ( E-bound ( L~ ( SpStSeq ( L~ f)))) & (p `1 ) >= ( W-bound ( L~ ( SpStSeq ( L~ f)))) & (p `2 ) = ( N-bound ( L~ ( SpStSeq ( L~ f)))) or (p `1 ) <= ( E-bound ( L~ ( SpStSeq ( L~ f)))) & (p `1 ) >= ( W-bound ( L~ ( SpStSeq ( L~ f)))) & (p `2 ) = ( S-bound ( L~ ( SpStSeq ( L~ f)))) or (p `1 ) = ( E-bound ( L~ ( SpStSeq ( L~ f)))) & (p `2 ) <= ( N-bound ( L~ ( SpStSeq ( L~ f)))) & (p `2 ) >= ( S-bound ( L~ ( SpStSeq ( L~ f)))) by A12, A18;

      

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

      consider r,s be Real such that

       A23: x = |[r, s]| and

       A24: ((G * (i,1)) `1 ) < r and

       A25: r < ((G * ((i + 1),1)) `1 ) and

       A26: ((G * (1,j)) `2 ) < s and

       A27: s < ((G * (1,(j + 1))) `2 ) by A6, A11;

      

       A28: (p `1 ) = r by A23, A20, EUCLID: 52;

      

       A29: (p `2 ) = s by A23, A20, EUCLID: 52;

      per cases by A21;

        suppose

         A30: (p `1 ) = ( W-bound ( L~ ( SpStSeq ( L~ f))));

        

         A31: 1 in ( dom <*(G * (i,1))*>) by FINSEQ_5: 6;

        ( <*(G * (i,1))*> /. 1) = (G * (i,1)) by FINSEQ_4: 16;

        hence contradiction by A24, A9, A28, A13, A30, A31;

      end;

        suppose

         A32: (p `2 ) = ( N-bound ( L~ ( SpStSeq ( L~ f))));

        

         A33: 1 in ( dom <*(G * (1,(j + 1)))*>) by FINSEQ_5: 6;

        ( <*(G * (1,(j + 1)))*> /. 1) = (G * (1,(j + 1))) by FINSEQ_4: 16;

        hence contradiction by A27, A17, A29, A7, A32, A33;

      end;

        suppose that

         A34: (p `2 ) = ( S-bound ( L~ ( SpStSeq ( L~ f))));

        

         A35: 1 in ( dom <*(G * (1,j))*>) by FINSEQ_5: 6;

        ( <*(G * (1,j))*> /. 1) = (G * (1,j)) by FINSEQ_4: 16;

        hence contradiction by A26, A15, A29, A22, A34, A35;

      end;

        suppose that

         A36: (p `1 ) = ( E-bound ( L~ ( SpStSeq ( L~ f))));

        

         A37: 1 in ( dom <*(G * ((i + 1),1))*>) by FINSEQ_5: 6;

        ( <*(G * ((i + 1),1))*> /. 1) = (G * ((i + 1),1)) by FINSEQ_4: 16;

        hence contradiction by A25, A10, A28, A19, A36, A37;

      end;

    end;

    theorem :: SPRECT_3:56

    for f,g be FinSequence of ( TOP-REAL 2), p be Point of ( TOP-REAL 2) st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in ( L~ g) holds ( L_Cut (g,p)) is_in_the_area_of f

    proof

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

       A1: g is_in_the_area_of f and

       A2: <*p*> is_in_the_area_of f and

       A3: g is being_S-Seq;

      2 <= ( len g) by A3, TOPREAL1:def 8;

      then 1 <= ( len g) by XXREAL_0: 2;

      then

       A4: ( len g) in ( dom g) by FINSEQ_3: 25;

      assume p in ( L~ g);

      then ( Index (p,g)) < ( len g) by JORDAN3: 8;

      then

       A5: (( Index (p,g)) + 1) <= ( len g) by NAT_1: 13;

      1 <= (( Index (p,g)) + 1) by NAT_1: 11;

      then

       A6: (( Index (p,g)) + 1) in ( dom g) by A5, FINSEQ_3: 25;

      per cases ;

        suppose p <> (g . (( Index (p,g)) + 1));

        then

         A7: ( L_Cut (g,p)) = ( <*p*> ^ ( mid (g,(( Index (p,g)) + 1),( len g)))) by JORDAN3:def 3;

        ( mid (g,(( Index (p,g)) + 1),( len g))) is_in_the_area_of f by A1, A4, A6, SPRECT_2: 22;

        hence thesis by A2, A7, SPRECT_2: 24;

      end;

        suppose p = (g . (( Index (p,g)) + 1));

        then ( L_Cut (g,p)) = ( mid (g,(( Index (p,g)) + 1),( len g))) by JORDAN3:def 3;

        hence thesis by A1, A4, A6, SPRECT_2: 22;

      end;

    end;