topreal4.miz



    begin

    reserve P,P1,P2,R for Subset of ( TOP-REAL 2),

p,p1,p2,p3,p11,p22,q,q1,q2,q3,q4 for Point of ( TOP-REAL 2),

f,h for FinSequence of ( TOP-REAL 2),

r for Real,

u for Point of ( Euclid 2),

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

x,y for set;

    definition

      let P, p, q;

      :: TOPREAL4:def1

      pred P is_S-P_arc_joining p,q means ex f st f is being_S-Seq & P = ( L~ f) & p = (f /. 1) & q = (f /. ( len f));

    end

    definition

      let P;

      :: TOPREAL4:def2

      attr P is being_special_polygon means ex p1, p2, P1, P2 st p1 <> p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining (p1,p2) & P2 is_S-P_arc_joining (p1,p2) & (P1 /\ P2) = {p1, p2} & P = (P1 \/ P2);

    end

    definition

      let T be TopStruct, P be Subset of T;

      :: TOPREAL4:def3

      attr P is being_Region means P is open connected;

    end

    theorem :: TOPREAL4:1

    

     Th1: P is_S-P_arc_joining (p,q) implies P is being_S-P_arc;

    theorem :: TOPREAL4:2

    

     Th2: P is_S-P_arc_joining (p,q) implies P is_an_arc_of (p,q) by TOPREAL1: 25;

    theorem :: TOPREAL4:3

    

     Th3: P is_S-P_arc_joining (p,q) implies p in P & q in P

    proof

      assume P is_S-P_arc_joining (p,q);

      then P is_an_arc_of (p,q) by Th2;

      hence thesis by TOPREAL1: 1;

    end;

    theorem :: TOPREAL4:4

    P is_S-P_arc_joining (p,q) implies p <> q

    proof

      assume that

       A1: P is_S-P_arc_joining (p,q) and

       A2: p = q;

      consider f such that

       A3: f is being_S-Seq and P = ( L~ f) and

       A4: p = (f /. 1) & q = (f /. ( len f)) by A1;

      ( len f) >= 2 by A3;

      then ( Seg ( len f)) = ( dom f) & ( len f) >= 1 by FINSEQ_1:def 3, XXREAL_0: 2;

      then

       A5: ( len f) in ( dom f) & 1 in ( dom f) by FINSEQ_1: 1;

      f is one-to-one & 1 <> ( len f) by A3;

      hence contradiction by A2, A4, A5, PARTFUN2: 10;

    end;

    theorem :: TOPREAL4:5

    P is being_special_polygon implies P is being_simple_closed_curve

    proof

      given p1, p2, P1, P2 such that

       A1: p1 <> p2 & p1 in P & p2 in P and

       A2: P1 is_S-P_arc_joining (p1,p2) & P2 is_S-P_arc_joining (p1,p2) and

       A3: (P1 /\ P2) = {p1, p2} and

       A4: P = (P1 \/ P2);

      reconsider P1, P2 as non empty Subset of ( TOP-REAL 2) by A3;

      P1 is_an_arc_of (p1,p2) & P2 is_an_arc_of (p1,p2) by A2, Th2;

      hence thesis by A1, A3, A4, TOPREAL2: 6;

    end;

    theorem :: TOPREAL4:6

    

     Th6: (p `1 ) = (q `1 ) & (p `2 ) <> (q `2 ) & p in ( Ball (u,r)) & q in ( Ball (u,r)) & f = <*p, |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|, q*> implies f is being_S-Seq & (f /. 1) = p & (f /. ( len f)) = q & ( L~ f) is_S-P_arc_joining (p,q) & ( L~ f) c= ( Ball (u,r))

    proof

      assume that

       A1: (p `1 ) = (q `1 ) and

       A2: (p `2 ) <> (q `2 ) and

       A3: p in ( Ball (u,r)) & q in ( Ball (u,r)) and

       A4: f = <*p, |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|, q*>;

      thus

       A5: f is being_S-Seq & (f /. 1) = p & (f /. ( len f)) = q by A1, A2, A4, TOPREAL3: 36;

      p = |[(p `1 ), (p `2 )]| & q = |[(q `1 ), (q `2 )]| by EUCLID: 53;

      then |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]| in ( Ball (u,r)) by A1, A3, TOPREAL3: 23;

      then

       A6: ( LSeg (p, |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|)) c= ( Ball (u,r)) & ( LSeg ( |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|,q)) c= ( Ball (u,r)) by A3, TOPREAL3: 21;

      thus ( L~ f) is_S-P_arc_joining (p,q) by A5;

      ( L~ f) = (( LSeg (p, |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|)) \/ ( LSeg ( |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|,q))) by A4, TOPREAL3: 16;

      hence thesis by A6, XBOOLE_1: 8;

    end;

    theorem :: TOPREAL4:7

    

     Th7: (p `1 ) <> (q `1 ) & (p `2 ) = (q `2 ) & p in ( Ball (u,r)) & q in ( Ball (u,r)) & f = <*p, |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|, q*> implies f is being_S-Seq & (f /. 1) = p & (f /. ( len f)) = q & ( L~ f) is_S-P_arc_joining (p,q) & ( L~ f) c= ( Ball (u,r))

    proof

      assume that

       A1: (p `1 ) <> (q `1 ) and

       A2: (p `2 ) = (q `2 ) and

       A3: p in ( Ball (u,r)) & q in ( Ball (u,r)) and

       A4: f = <*p, |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|, q*>;

      thus

       A5: f is being_S-Seq & (f /. 1) = p & (f /. ( len f)) = q by A1, A2, A4, TOPREAL3: 37;

      p = |[(p `1 ), (p `2 )]| & q = |[(q `1 ), (q `2 )]| by EUCLID: 53;

      then |[(((p `1 ) + (q `1 )) / 2), (p `2 )]| in ( Ball (u,r)) by A2, A3, TOPREAL3: 24;

      then

       A6: ( LSeg (p, |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|)) c= ( Ball (u,r)) & ( LSeg ( |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|,q)) c= ( Ball (u,r)) by A3, TOPREAL3: 21;

      thus ( L~ f) is_S-P_arc_joining (p,q) by A5;

      ( L~ f) = (( LSeg (p, |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|)) \/ ( LSeg ( |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|,q))) by A4, TOPREAL3: 16;

      hence thesis by A6, XBOOLE_1: 8;

    end;

    theorem :: TOPREAL4:8

    

     Th8: (p `1 ) <> (q `1 ) & (p `2 ) <> (q `2 ) & p in ( Ball (u,r)) & q in ( Ball (u,r)) & |[(p `1 ), (q `2 )]| in ( Ball (u,r)) & f = <*p, |[(p `1 ), (q `2 )]|, q*> implies f is being_S-Seq & (f /. 1) = p & (f /. ( len f)) = q & ( L~ f) is_S-P_arc_joining (p,q) & ( L~ f) c= ( Ball (u,r))

    proof

      assume that

       A1: (p `1 ) <> (q `1 ) & (p `2 ) <> (q `2 ) and

       A2: p in ( Ball (u,r)) and

       A3: q in ( Ball (u,r)) and

       A4: |[(p `1 ), (q `2 )]| in ( Ball (u,r)) and

       A5: f = <*p, |[(p `1 ), (q `2 )]|, q*>;

      thus

       A6: f is being_S-Seq & (f /. 1) = p & (f /. ( len f)) = q by A1, A5, TOPREAL3: 34;

      

       A7: ( LSeg ( |[(p `1 ), (q `2 )]|,q)) c= ( Ball (u,r)) by A3, A4, TOPREAL3: 21;

      thus ( L~ f) is_S-P_arc_joining (p,q) by A6;

      ( L~ f) = (( LSeg (p, |[(p `1 ), (q `2 )]|)) \/ ( LSeg ( |[(p `1 ), (q `2 )]|,q))) & ( LSeg (p, |[(p `1 ), (q `2 )]|)) c= ( Ball (u,r)) by A2, A4, A5, TOPREAL3: 16, TOPREAL3: 21;

      hence thesis by A7, XBOOLE_1: 8;

    end;

    theorem :: TOPREAL4:9

    

     Th9: (p `1 ) <> (q `1 ) & (p `2 ) <> (q `2 ) & p in ( Ball (u,r)) & q in ( Ball (u,r)) & |[(q `1 ), (p `2 )]| in ( Ball (u,r)) & f = <*p, |[(q `1 ), (p `2 )]|, q*> implies f is being_S-Seq & (f /. 1) = p & (f /. ( len f)) = q & ( L~ f) is_S-P_arc_joining (p,q) & ( L~ f) c= ( Ball (u,r))

    proof

      assume that

       A1: (p `1 ) <> (q `1 ) & (p `2 ) <> (q `2 ) and

       A2: p in ( Ball (u,r)) and

       A3: q in ( Ball (u,r)) and

       A4: |[(q `1 ), (p `2 )]| in ( Ball (u,r)) and

       A5: f = <*p, |[(q `1 ), (p `2 )]|, q*>;

      thus

       A6: f is being_S-Seq & (f /. 1) = p & (f /. ( len f)) = q by A1, A5, TOPREAL3: 35;

      

       A7: ( LSeg ( |[(q `1 ), (p `2 )]|,q)) c= ( Ball (u,r)) by A3, A4, TOPREAL3: 21;

      thus ( L~ f) is_S-P_arc_joining (p,q) by A6;

      ( L~ f) = (( LSeg (p, |[(q `1 ), (p `2 )]|)) \/ ( LSeg ( |[(q `1 ), (p `2 )]|,q))) & ( LSeg (p, |[(q `1 ), (p `2 )]|)) c= ( Ball (u,r)) by A2, A4, A5, TOPREAL3: 16, TOPREAL3: 21;

      hence thesis by A7, XBOOLE_1: 8;

    end;

    theorem :: TOPREAL4:10

    

     Th10: p <> q & p in ( Ball (u,r)) & q in ( Ball (u,r)) implies ex P st P is_S-P_arc_joining (p,q) & P c= ( Ball (u,r))

    proof

      assume that

       A1: p <> q and

       A2: p in ( Ball (u,r)) & q in ( Ball (u,r));

      now

        per cases by A1, TOPREAL3: 6;

          suppose

           A3: (p `1 ) <> (q `1 );

          now

            per cases ;

              suppose

               A4: (p `2 ) = (q `2 );

              reconsider P = ( L~ <*p, |[(((p `1 ) + (q `1 )) / 2), (p `2 )]|, q*>) as Subset of ( TOP-REAL 2);

              take P;

              thus P is_S-P_arc_joining (p,q) & P c= ( Ball (u,r)) by A2, A3, A4, Th7;

            end;

              suppose

               A5: (p `2 ) <> (q `2 );

              

               A6: p = |[(p `1 ), (p `2 )]| & q = |[(q `1 ), (q `2 )]| by EUCLID: 53;

              now

                per cases by A2, A6, TOPREAL3: 25;

                  suppose

                   A7: |[(p `1 ), (q `2 )]| in ( Ball (u,r));

                  reconsider P = ( L~ <*p, |[(p `1 ), (q `2 )]|, q*>) as Subset of ( TOP-REAL 2);

                  take P;

                  thus P is_S-P_arc_joining (p,q) & P c= ( Ball (u,r)) by A2, A3, A5, A7, Th8;

                end;

                  suppose

                   A8: |[(q `1 ), (p `2 )]| in ( Ball (u,r));

                  reconsider P = ( L~ <*p, |[(q `1 ), (p `2 )]|, q*>) as Subset of ( TOP-REAL 2);

                  take P;

                  thus P is_S-P_arc_joining (p,q) & P c= ( Ball (u,r)) by A2, A3, A5, A8, Th9;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

          suppose

           A9: (p `2 ) <> (q `2 );

          now

            per cases ;

              suppose

               A10: (p `1 ) = (q `1 );

              reconsider P = ( L~ <*p, |[(p `1 ), (((p `2 ) + (q `2 )) / 2)]|, q*>) as Subset of ( TOP-REAL 2);

              take P;

              thus P is_S-P_arc_joining (p,q) & P c= ( Ball (u,r)) by A2, A9, A10, Th6;

            end;

              suppose

               A11: (p `1 ) <> (q `1 );

              

               A12: p = |[(p `1 ), (p `2 )]| & q = |[(q `1 ), (q `2 )]| by EUCLID: 53;

              now

                per cases by A2, A12, TOPREAL3: 25;

                  suppose

                   A13: |[(p `1 ), (q `2 )]| in ( Ball (u,r));

                  reconsider P = ( L~ <*p, |[(p `1 ), (q `2 )]|, q*>) as Subset of ( TOP-REAL 2);

                  take P;

                  thus P is_S-P_arc_joining (p,q) & P c= ( Ball (u,r)) by A2, A9, A11, A13, Th8;

                end;

                  suppose

                   A14: |[(q `1 ), (p `2 )]| in ( Ball (u,r));

                  reconsider P = ( L~ <*p, |[(q `1 ), (p `2 )]|, q*>) as Subset of ( TOP-REAL 2);

                  take P;

                  thus P is_S-P_arc_joining (p,q) & P c= ( Ball (u,r)) by A2, A9, A11, A14, Th9;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL4:11

    

     Th11: p <> (f /. 1) & ((f /. 1) `2 ) = (p `2 ) & f is being_S-Seq & p in ( LSeg (f,1)) & h = <*(f /. 1), |[((((f /. 1) `1 ) + (p `1 )) / 2), ((f /. 1) `2 )]|, p*> implies h is being_S-Seq & (h /. 1) = (f /. 1) & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining ((f /. 1),p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | 1)) \/ ( LSeg ((f /. 1),p)))

    proof

      assume that

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

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

       A3: f is being_S-Seq and

       A4: p in ( LSeg (f,1)) and

       A5: h = <*(f /. 1), |[((((f /. 1) `1 ) + (p `1 )) / 2), ((f /. 1) `2 )]|, p*>;

      set p1 = (f /. 1), q = (f /. (1 + 1));

      

       A6: ( L~ h) = (( LSeg (p1, |[(((p1 `1 ) + (p `1 )) / 2), (p1 `2 )]|)) \/ ( LSeg ( |[(((p1 `1 ) + (p `1 )) / 2), (p1 `2 )]|,p))) by A5, TOPREAL3: 16;

      

       A7: ( len f) >= 2 by A3;

      then

       A8: ( LSeg (f,1)) = ( LSeg (p1,q)) by TOPREAL1:def 3;

      

       A9: (p1 `1 ) <> (p `1 ) by A1, A2, TOPREAL3: 6;

      hence

       A10: h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p by A2, A5, TOPREAL3: 37;

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

      then

       A11: ( LSeg (p1,p)) c= ( LSeg (p1,q)) by A4, A8, TOPREAL1: 6;

      

       A12: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      thus ( L~ h) is_S-P_arc_joining (p1,p) by A10;

      

       A13: ( LSeg (f,1)) c= ( L~ f) by TOPREAL3: 19;

      (( LSeg (p1, |[(((p1 `1 ) + (p `1 )) / 2), (p1 `2 )]|)) \/ ( LSeg ( |[(((p1 `1 ) + (p `1 )) / 2), (p1 `2 )]|,p))) = ( LSeg (p1,p)) by A2, A9, TOPREAL1: 5, TOPREAL3: 13;

      hence ( L~ h) c= ( L~ f) by A8, A11, A6, A13;

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

      then ( Seg 1) c= ( Seg ( len f)) by FINSEQ_1: 5;

      then (f | 1) = (f | ( Seg 1)) & (( dom f) /\ ( Seg 1)) = ( Seg 1) by A12, FINSEQ_1:def 15, XBOOLE_1: 28;

      then ( dom (f | 1)) = ( Seg 1) by RELAT_1: 61;

      then ( len (f | 1)) = 1 by FINSEQ_1:def 3;

      then ( L~ (f | 1)) = {} by TOPREAL1: 22;

      hence thesis by A2, A9, A6, TOPREAL1: 5, TOPREAL3: 13;

    end;

    theorem :: TOPREAL4:12

    

     Th12: p <> (f /. 1) & ((f /. 1) `1 ) = (p `1 ) & f is being_S-Seq & p in ( LSeg (f,1)) & h = <*(f /. 1), |[((f /. 1) `1 ), ((((f /. 1) `2 ) + (p `2 )) / 2)]|, p*> implies h is being_S-Seq & (h /. 1) = (f /. 1) & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining ((f /. 1),p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | 1)) \/ ( LSeg ((f /. 1),p)))

    proof

      set p1 = (f /. 1);

      assume that

       A1: p <> p1 and

       A2: (p1 `1 ) = (p `1 ) and

       A3: f is being_S-Seq and

       A4: p in ( LSeg (f,1)) and

       A5: h = <*p1, |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|, p*>;

      

       A6: ( L~ h) = (( LSeg (p1, |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|)) \/ ( LSeg ( |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|,p))) by A5, TOPREAL3: 16;

      set q = (f /. (1 + 1));

      

       A7: ( len f) >= 2 by A3;

      then

       A8: ( LSeg (f,1)) = ( LSeg (p1,q)) by TOPREAL1:def 3;

      

       A9: (p1 `2 ) <> (p `2 ) by A1, A2, TOPREAL3: 6;

      hence

       A10: h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p by A2, A5, TOPREAL3: 36;

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

      then

       A11: ( LSeg (p1,p)) c= ( LSeg (p1,q)) by A4, A8, TOPREAL1: 6;

      

       A12: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      thus ( L~ h) is_S-P_arc_joining (p1,p) by A10;

      

       A13: ( LSeg (f,1)) c= ( L~ f) by TOPREAL3: 19;

      (( LSeg (p1, |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|)) \/ ( LSeg ( |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|,p))) = ( LSeg (p1,p)) by A2, A9, TOPREAL1: 5, TOPREAL3: 14;

      hence ( L~ h) c= ( L~ f) by A8, A11, A6, A13;

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

      then ( Seg 1) c= ( Seg ( len f)) by FINSEQ_1: 5;

      then (f | 1) = (f | ( Seg 1)) & (( dom f) /\ ( Seg 1)) = ( Seg 1) by A12, FINSEQ_1:def 15, XBOOLE_1: 28;

      then ( dom (f | 1)) = ( Seg 1) by RELAT_1: 61;

      then ( len (f | 1)) = 1 by FINSEQ_1:def 3;

      then ( L~ (f | 1)) = {} by TOPREAL1: 22;

      hence thesis by A2, A9, A6, TOPREAL1: 5, TOPREAL3: 14;

    end;

    theorem :: TOPREAL4:13

    

     Th13: f is being_S-Seq & i in ( dom f) & (i + 1) in ( dom f) & i > 1 & p in ( LSeg (f,i)) & p <> (f /. i) & h = ((f | i) ^ <*p*>) implies h is being_S-Seq & (h /. 1) = (f /. 1) & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining ((f /. 1),p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | i)) \/ ( LSeg ((f /. i),p)))

    proof

      set p1 = (f /. 1), q = (f /. i);

      assume that

       A1: f is being_S-Seq and

       A2: i in ( dom f) and

       A3: (i + 1) in ( dom f) and

       A4: i > 1 and

       A5: p in ( LSeg (f,i)) and

       A6: p <> (f /. i) and

       A7: h = ((f | i) ^ <*p*>);

      

       A8: f is one-to-one by A1;

      set v = (f | i);

      

       A9: v = (f | ( Seg i)) by FINSEQ_1:def 15;

      then

       A10: ( dom v) = (( dom f) /\ ( Seg i)) by RELAT_1: 61;

      

       A11: ( Seg ( len h)) = ( dom h) by FINSEQ_1:def 3;

      

       A12: f is unfolded by A1;

      

       A13: f is special by A1;

      

       A14: f is s.n.c. by A1;

      set q1 = (f /. i), q2 = (f /. (i + 1));

      

       A15: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      then

       A16: (i + 1) <= ( len f) by A3, FINSEQ_1: 1;

      then

       A17: p in ( LSeg (q1,q2)) by A4, A5, TOPREAL1:def 3;

      

       A18: ( LSeg (f,i)) = ( LSeg (q1,q2)) by A4, A16, TOPREAL1:def 3;

      

       A19: ( LSeg (f,i)) = ( LSeg (q2,q1)) by A4, A16, TOPREAL1:def 3;

      i <> (i + 1);

      then

       A20: q1 <> q2 by A2, A3, A8, PARTFUN2: 10;

      

       A21: q1 in ( LSeg (q1,q2)) by RLTOPSP1: 68;

      

       A22: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

      

       A23: i in NAT by ORDINAL1:def 12;

      

       A24: i <= ( len f) by A2, A15, FINSEQ_1: 1;

      then ( Seg i) c= ( dom f) by A15, FINSEQ_1: 5;

      then

       A25: ( dom v) = ( Seg i) by A10, XBOOLE_1: 28;

      then

       A26: ( len v) = i by FINSEQ_1:def 3, A23;

      

      then

       A27: ( len h) = (i + ( len <*p*>)) by A7, FINSEQ_1: 22

      .= (i + 1) by FINSEQ_1: 39;

      then

       A28: (h /. ( len h)) = p by A7, A26, FINSEQ_4: 67;

      

       A29: i in ( dom v) by A4, A25, FINSEQ_1: 1;

      

      then

       A30: (h /. i) = (v /. i) by A7, FINSEQ_4: 68

      .= q1 by A29, FINSEQ_4: 70;

      then

       A31: ( LSeg (h,i)) = ( LSeg (q1,p)) by A4, A27, A28, TOPREAL1:def 3;

      

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

      thus

       A33: h is being_S-Seq

      proof

        now

          set Z = { m where m be Nat : 1 <= m & m <= ( len h) };

          given x,y be object such that

           A34: x in ( dom h) and

           A35: y in ( dom h) and

           A36: (h . x) = (h . y) and

           A37: x <> y;

          x in Z by A11, A34, FINSEQ_1:def 1;

          then

          consider k1 be Nat such that

           A38: k1 = x and

           A39: 1 <= k1 and

           A40: k1 <= ( len h);

          y in Z by A11, A35, FINSEQ_1:def 1;

          then

          consider k2 be Nat such that

           A41: k2 = y and

           A42: 1 <= k2 and

           A43: k2 <= ( len h);

          

           A44: (h /. k1) = (h . y) by A34, A36, A38, PARTFUN1:def 6

          .= (h /. k2) by A35, A41, PARTFUN1:def 6;

          k2 <= ( len f) by A27, A16, A43, XXREAL_0: 2;

          then

           A45: k2 in ( dom f) by A15, A42, FINSEQ_1: 1;

          k1 <= ( len f) by A27, A16, A40, XXREAL_0: 2;

          then

           A46: k1 in ( dom f) by A15, A39, FINSEQ_1: 1;

          

           A47: (k1 + (1 + 1)) = ((k1 + 1) + 1);

          

           A48: (k2 + (1 + 1)) = ((k2 + 1) + 1);

          now

            per cases by A27, A40, A43, XXREAL_0: 1;

              suppose k1 = (i + 1) & k2 = (i + 1);

              hence contradiction by A37, A38, A41;

            end;

              suppose

               A49: k1 = (i + 1) & k2 < (i + 1);

              then

               A50: (k2 + 1) <= k1 by NAT_1: 13;

              now

                per cases by A50, XXREAL_0: 1;

                  suppose (k2 + 1) = k1;

                  hence contradiction by A6, A7, A26, A30, A44, A49, FINSEQ_4: 67;

                end;

                  suppose (k2 + 1) < k1;

                  then

                   A51: (k2 + 1) <= i by A49, NAT_1: 13;

                  now

                    per cases by A51, XXREAL_0: 1;

                      suppose

                       A52: (k2 + 1) = i;

                      then k2 <= i by NAT_1: 11;

                      then

                       A53: k2 in ( dom v) by A25, A42, FINSEQ_1: 1;

                      

                      then

                       A54: (h /. k2) = (v /. k2) by A7, FINSEQ_4: 68

                      .= (f /. k2) by A53, FINSEQ_4: 70;

                      (k2 + 1) <= ( len f) by A2, A15, A52, FINSEQ_1: 1;

                      then

                       A55: (f /. k2) in ( LSeg (f,k2)) by A42, TOPREAL1: 21;

                      (( LSeg (f,k2)) /\ ( LSeg (f,i))) = {(f /. i)} by A12, A16, A42, A48, A52;

                      then (f /. k2) in {(f /. i)} by A5, A27, A28, A44, A49, A55, A54, XBOOLE_0:def 4;

                      then

                       A56: (f /. k2) = (f /. i) by TARSKI:def 1;

                      k2 < i by A52, NAT_1: 13;

                      hence contradiction by A2, A8, A45, A56, PARTFUN2: 10;

                    end;

                      suppose

                       A57: (k2 + 1) < i;

                      then

                       A58: (k2 + 1) <= ( len f) by A24, XXREAL_0: 2;

                      

                       A59: ( LSeg (f,k2)) misses ( LSeg (f,i)) by A14, A57;

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

                      then k2 <= i by A57, XXREAL_0: 2;

                      then

                       A60: k2 in ( dom v) by A25, A42, FINSEQ_1: 1;

                      

                      then (h /. k2) = (v /. k2) by A7, FINSEQ_4: 68

                      .= (f /. k2) by A60, FINSEQ_4: 70;

                      then p in ( LSeg (f,k2)) by A27, A28, A42, A44, A49, A58, TOPREAL1: 21;

                      hence contradiction by A5, A59, XBOOLE_0: 3;

                    end;

                  end;

                  hence contradiction;

                end;

              end;

              hence contradiction;

            end;

              suppose

               A61: k1 < (i + 1) & k2 = (i + 1);

              then

               A62: (k1 + 1) <= k2 by NAT_1: 13;

              now

                per cases by A62, XXREAL_0: 1;

                  suppose (k1 + 1) = k2;

                  hence contradiction by A6, A7, A26, A30, A44, A61, FINSEQ_4: 67;

                end;

                  suppose (k1 + 1) < k2;

                  then

                   A63: (k1 + 1) <= i by A61, NAT_1: 13;

                  now

                    per cases by A63, XXREAL_0: 1;

                      suppose

                       A64: (k1 + 1) = i;

                      then k1 <= i by NAT_1: 11;

                      then

                       A65: k1 in ( dom v) by A25, A39, FINSEQ_1: 1;

                      

                      then

                       A66: (h /. k1) = (v /. k1) by A7, FINSEQ_4: 68

                      .= (f /. k1) by A65, FINSEQ_4: 70;

                      (k1 + 1) <= ( len f) by A2, A15, A64, FINSEQ_1: 1;

                      then

                       A67: (f /. k1) in ( LSeg (f,k1)) by A39, TOPREAL1: 21;

                      (( LSeg (f,k1)) /\ ( LSeg (f,i))) = {(f /. i)} by A12, A16, A39, A47, A64;

                      then (f /. k1) in {(f /. i)} by A5, A27, A28, A44, A61, A67, A66, XBOOLE_0:def 4;

                      then

                       A68: (f /. k1) = (f /. i) by TARSKI:def 1;

                      k1 < i by A64, NAT_1: 13;

                      hence contradiction by A2, A8, A46, A68, PARTFUN2: 10;

                    end;

                      suppose

                       A69: (k1 + 1) < i;

                      then

                       A70: (k1 + 1) <= ( len f) by A24, XXREAL_0: 2;

                      

                       A71: ( LSeg (f,k1)) misses ( LSeg (f,i)) by A14, A69;

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

                      then k1 <= i by A69, XXREAL_0: 2;

                      then

                       A72: k1 in ( dom v) by A25, A39, FINSEQ_1: 1;

                      

                      then (h /. k1) = (v /. k1) by A7, FINSEQ_4: 68

                      .= (f /. k1) by A72, FINSEQ_4: 70;

                      then p in ( LSeg (f,k1)) by A27, A28, A39, A44, A61, A70, TOPREAL1: 21;

                      hence contradiction by A5, A71, XBOOLE_0: 3;

                    end;

                  end;

                  hence contradiction;

                end;

              end;

              hence contradiction;

            end;

              suppose

               A73: k1 < (i + 1) & k2 < (i + 1);

              then k2 <= i by NAT_1: 13;

              then

               A74: k2 in ( dom v) by A25, A42, FINSEQ_1: 1;

              k1 <= i by A73, NAT_1: 13;

              then

               A75: k1 in ( dom v) by A25, A39, FINSEQ_1: 1;

              

              then (f . k1) = (v . k1) by A9, FUNCT_1: 47

              .= (h . k1) by A7, A75, FINSEQ_1:def 7

              .= (v . k2) by A7, A36, A38, A41, A74, FINSEQ_1:def 7

              .= (f . k2) by A9, A74, FUNCT_1: 47;

              hence contradiction by A8, A37, A38, A41, A46, A45, FUNCT_1:def 4;

            end;

          end;

          hence contradiction;

        end;

        hence h is one-to-one by FUNCT_1:def 4;

        thus ( len h) >= 2 by A4, A27, A32, XREAL_1: 6;

        thus h is unfolded

        proof

          let j be Nat such that

           A76: 1 <= j and

           A77: (j + 2) <= ( len h);

          

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

          ((j + 1) + 1) = (j + (1 + 1));

          then (j + 1) <= i by A27, A77, XREAL_1: 6;

          then

           A79: (j + 1) in ( dom v) by A25, A78, FINSEQ_1: 1;

          

          then

           A80: (h /. (j + 1)) = (v /. (j + 1)) by A7, FINSEQ_4: 68

          .= (f /. (j + 1)) by A79, FINSEQ_4: 70;

          ((i + 1) + 1) = (i + (1 + 1));

          then ( len h) <= (i + 2) by A27, NAT_1: 11;

          then (j + 2) <= (i + 2) by A77, XXREAL_0: 2;

          then j <= i by XREAL_1: 6;

          then

           A81: j in ( dom v) by A25, A76, FINSEQ_1: 1;

          

          then

           A82: ( LSeg (h,j)) = ( LSeg (v,j)) by A7, A79, TOPREAL3: 18

          .= ( LSeg (f,j)) by A81, A79, TOPREAL3: 17;

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

          then

           A83: 1 <= (j + (1 + 1)) by A76, XXREAL_0: 2;

          

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

          (i + 1) in ( Seg ( len f)) by A3, FINSEQ_1:def 3;

          then ( len h) <= ( len f) by A27, FINSEQ_1: 1;

          then

           A85: (j + 2) <= ( len f) by A77, XXREAL_0: 2;

          then

           A86: (( LSeg (f,j)) /\ ( LSeg (f,(j + 1)))) = {(f /. (j + 1))} by A12, A76;

          now

            per cases by A77, XXREAL_0: 1;

              suppose

               A87: (j + 2) = ( len h);

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

              then (j + 1) <= ( len h) by A77, XXREAL_0: 2;

              then

               A88: (h /. (j + 1)) in ( LSeg (h,j)) by A76, TOPREAL1: 21;

              (h /. (j + 1)) in ( LSeg (h,(j + 1))) by A77, A78, A84, TOPREAL1: 21;

              then (h /. (j + 1)) in (( LSeg (h,j)) /\ ( LSeg (h,(j + 1)))) by A88, XBOOLE_0:def 4;

              then

               A89: {(h /. (j + 1))} c= (( LSeg (h,j)) /\ ( LSeg (h,(j + 1)))) by ZFMISC_1: 31;

              (( LSeg (h,j)) /\ ( LSeg (h,(j + 1)))) c= {(h /. (j + 1))} by A27, A18, A21, A17, A31, A86, A82, A80, A87, TOPREAL1: 6, XBOOLE_1: 26;

              hence thesis by A89;

            end;

              suppose (j + 2) < ( len h);

              then (j + (1 + 1)) <= i by A27, NAT_1: 13;

              then

               A90: ((j + 1) + 1) in ( dom v) by A25, A83, FINSEQ_1: 1;

              

              then ( LSeg (h,(j + 1))) = ( LSeg (v,(j + 1))) by A7, A79, TOPREAL3: 18

              .= ( LSeg (f,(j + 1))) by A79, A90, TOPREAL3: 17;

              hence thesis by A12, A76, A85, A82, A80;

            end;

          end;

          hence thesis;

        end;

        thus h is s.n.c.

        proof

          let n,m be Nat;

          assume

           A91: m > (n + 1);

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

          then

           A92: n <= m by A91, XXREAL_0: 2;

          

           A93: 1 <= (n + 1) by NAT_1: 11;

          

           A94: ( LSeg (f,n)) misses ( LSeg (f,m)) by A14, A91;

          now

            per cases by XXREAL_0: 1;

              suppose

               A95: (m + 1) < ( len h);

              

               A96: 1 < m by A91, A93, XXREAL_0: 2;

              then

               A97: 1 <= (m + 1) by NAT_1: 13;

              (m + 1) <= i by A27, A95, NAT_1: 13;

              then

               A98: (m + 1) in ( dom v) by A25, A97, FINSEQ_1: 1;

              

               A99: m <= i by A27, A95, XREAL_1: 6;

              then

               A100: m in ( dom v) by A25, A96, FINSEQ_1: 1;

              

              then

               A101: ( LSeg (h,m)) = ( LSeg (v,m)) by A7, A98, TOPREAL3: 18

              .= ( LSeg (f,m)) by A100, A98, TOPREAL3: 17;

              now

                per cases ;

                  suppose 0 < n;

                  then

                   A102: ( 0 + 1) <= n by NAT_1: 13;

                  (n + 1) <= i by A91, A99, XXREAL_0: 2;

                  then

                   A103: (n + 1) in ( dom v) by A25, A93, FINSEQ_1: 1;

                  n <= i by A92, A99, XXREAL_0: 2;

                  then

                   A104: n in ( dom v) by A25, A102, FINSEQ_1: 1;

                  

                  then ( LSeg (h,n)) = ( LSeg (v,n)) by A7, A103, TOPREAL3: 18

                  .= ( LSeg (f,n)) by A104, A103, TOPREAL3: 17;

                  then ( LSeg (h,n)) misses ( LSeg (h,m)) by A14, A91, A101;

                  hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

                end;

                  suppose 0 = n;

                  then ( LSeg (h,n)) = {} by TOPREAL1:def 3;

                  hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

                end;

              end;

              hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

            end;

              suppose

               A105: (m + 1) = ( len h);

              

               A106: (( LSeg (f,n)) /\ ( LSeg (f,m))) = {} by A94;

              now

                per cases ;

                  suppose 0 < n;

                  then ( 0 + 1) <= n by NAT_1: 13;

                  then

                   A107: n in ( dom v) by A25, A27, A92, A105, FINSEQ_1: 1;

                  

                   A108: (n + 1) in ( dom v) by A25, A27, A91, A93, A105, FINSEQ_1: 1;

                  

                  then ( LSeg (h,n)) = ( LSeg (v,n)) by A7, A107, TOPREAL3: 18

                  .= ( LSeg (f,n)) by A107, A108, TOPREAL3: 17;

                  

                  hence {} = (( LSeg (h,m)) /\ (( LSeg (f,m)) /\ ( LSeg (h,n)))) by A106

                  .= ((( LSeg (h,m)) /\ ( LSeg (f,m))) /\ ( LSeg (h,n))) by XBOOLE_1: 16

                  .= (( LSeg (h,n)) /\ ( LSeg (h,m))) by A27, A18, A21, A17, A31, A105, TOPREAL1: 6, XBOOLE_1: 28;

                end;

                  suppose 0 = n;

                  then ( LSeg (h,n)) = {} by TOPREAL1:def 3;

                  hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

                end;

              end;

              hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

            end;

              suppose (m + 1) > ( len h);

              then ( LSeg (h,m)) = {} by TOPREAL1:def 3;

              hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

            end;

          end;

          hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

        end;

        let n be Nat such that

         A109: 1 <= n and

         A110: (n + 1) <= ( len h);

        set p3 = (h /. n), p4 = (h /. (n + 1));

        now

          per cases by A110, XXREAL_0: 1;

            suppose

             A111: (n + 1) = ( len h);

            

             A112: i in ( dom v) by A4, A25, FINSEQ_1: 1;

            

            then

             A113: p3 = (v /. i) by A7, A27, A111, FINSEQ_4: 68

            .= q1 by A112, FINSEQ_4: 70;

            now

              per cases by A4, A13, A16;

                suppose

                 A114: (q1 `1 ) = (q2 `1 );

                then

                 A115: (q1 `2 ) <> (q2 `2 ) by A20, TOPREAL3: 6;

                now

                  per cases by A115, XXREAL_0: 1;

                    suppose (q1 `2 ) < (q2 `2 );

                    then p in { p11 : (p11 `1 ) = (q1 `1 ) & (q1 `2 ) <= (p11 `2 ) & (p11 `2 ) <= (q2 `2 ) } by A5, A19, A22, A114, TOPREAL3: 9;

                    then ex p11 st p = p11 & (p11 `1 ) = (q1 `1 ) & (q1 `2 ) <= (p11 `2 ) & (p11 `2 ) <= (q2 `2 );

                    hence thesis by A7, A26, A27, A111, A113, FINSEQ_4: 67;

                  end;

                    suppose (q2 `2 ) < (q1 `2 );

                    then p in { p22 : (p22 `1 ) = (q1 `1 ) & (q2 `2 ) <= (p22 `2 ) & (p22 `2 ) <= (q1 `2 ) } by A5, A19, A22, A114, TOPREAL3: 9;

                    then ex p11 st p = p11 & (p11 `1 ) = (q1 `1 ) & (q2 `2 ) <= (p11 `2 ) & (p11 `2 ) <= (q1 `2 );

                    hence thesis by A7, A26, A27, A111, A113, FINSEQ_4: 67;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A116: (q1 `2 ) = (q2 `2 );

                then

                 A117: (q1 `1 ) <> (q2 `1 ) by A20, TOPREAL3: 6;

                now

                  per cases by A117, XXREAL_0: 1;

                    suppose (q1 `1 ) < (q2 `1 );

                    then p in { p11 : (p11 `2 ) = (q1 `2 ) & (q1 `1 ) <= (p11 `1 ) & (p11 `1 ) <= (q2 `1 ) } by A5, A19, A22, A116, TOPREAL3: 10;

                    then ex p11 st p = p11 & (p11 `2 ) = (q1 `2 ) & (q1 `1 ) <= (p11 `1 ) & (p11 `1 ) <= (q2 `1 );

                    hence thesis by A7, A26, A27, A111, A113, FINSEQ_4: 67;

                  end;

                    suppose (q2 `1 ) < (q1 `1 );

                    then p in { p22 : (p22 `2 ) = (q1 `2 ) & (q2 `1 ) <= (p22 `1 ) & (p22 `1 ) <= (q1 `1 ) } by A5, A19, A22, A116, TOPREAL3: 10;

                    then ex p11 st p = p11 & (p11 `2 ) = (q1 `2 ) & (q2 `1 ) <= (p11 `1 ) & (p11 `1 ) <= (q1 `1 );

                    hence thesis by A7, A26, A27, A111, A113, FINSEQ_4: 67;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

            suppose

             A118: (n + 1) < ( len h);

            

             A119: 1 <= (n + 1) by A109, NAT_1: 13;

            (n + 1) <= i by A27, A118, NAT_1: 13;

            then

             A120: (n + 1) in ( dom v) by A25, A119, FINSEQ_1: 1;

            then (h /. (n + 1)) = (v /. (n + 1)) by A7, FINSEQ_4: 68;

            then

             A121: p4 = (f /. (n + 1)) by A120, FINSEQ_4: 70;

            n <= i by A27, A118, XREAL_1: 6;

            then

             A122: n in ( dom v) by A25, A109, FINSEQ_1: 1;

            then (h /. n) = (v /. n) by A7, FINSEQ_4: 68;

            then

             A123: p3 = (f /. n) by A122, FINSEQ_4: 70;

            (n + 1) <= ( len f) by A27, A16, A110, XXREAL_0: 2;

            hence thesis by A13, A109, A123, A121;

          end;

        end;

        hence thesis;

      end;

      

       A124: 1 in ( dom v) by A4, A25, FINSEQ_1: 1;

      

      then (h /. 1) = (v /. 1) by A7, FINSEQ_4: 68

      .= p1 by A124, FINSEQ_4: 70;

      hence

       A125: (h /. 1) = p1 & (h /. ( len h)) = p by A7, A26, A27, FINSEQ_4: 67;

      set Mf = { ( LSeg (f,j)) : 1 <= j & (j + 1) <= ( len f) }, Mv = { ( LSeg (v,n)) : 1 <= n & (n + 1) <= ( len v) }, Mh = { ( LSeg (h,m)) : 1 <= m & (m + 1) <= ( len h) };

      

       A126: ( Seg ( len v)) = ( dom v) by FINSEQ_1:def 3;

      thus ( L~ h) is_S-P_arc_joining (p1,p) by A33, A125;

       A127:

      now

        let x;

        assume x in ( L~ h);

        then

        consider X be set such that

         A128: x in X and

         A129: X in Mh by TARSKI:def 4;

        consider k such that

         A130: X = ( LSeg (h,k)) and

         A131: 1 <= k and

         A132: (k + 1) <= ( len h) by A129;

        

         A133: (k + 1) <= ( len f) by A27, A16, A132, XXREAL_0: 2;

        now

          per cases by A132, XXREAL_0: 1;

            suppose

             A134: (k + 1) = ( len h);

            then

             A135: ( LSeg (f,k)) in Mf by A27, A16, A131;

            ( LSeg (h,i)) c= ( LSeg (f,i)) by A5, A18, A21, A31, TOPREAL1: 6;

            hence x in ( L~ f) by A27, A128, A130, A134, A135, TARSKI:def 4;

            thus x in (( L~ v) \/ ( LSeg (q1,p))) by A27, A31, A128, A130, A134, XBOOLE_0:def 3;

          end;

            suppose

             A136: (k + 1) < ( len h);

            then

             A137: (k + 1) <= ( len v) by A26, A27, NAT_1: 13;

            

             A138: (k + 1) <= i by A27, A136, NAT_1: 13;

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

            then k <= i by A138, XXREAL_0: 2;

            then

             A139: k in ( dom v) by A25, A131, FINSEQ_1: 1;

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

            then

             A140: (k + 1) in ( dom v) by A25, A138, FINSEQ_1: 1;

            

            then

             A141: X = ( LSeg (v,k)) by A7, A130, A139, TOPREAL3: 18

            .= ( LSeg (f,k)) by A140, A139, TOPREAL3: 17;

            then X in Mf by A131, A133;

            hence x in ( L~ f) by A128, TARSKI:def 4;

            X = ( LSeg (v,k)) by A140, A139, A141, TOPREAL3: 17;

            then X in Mv by A131, A137;

            then x in ( union Mv) by A128, TARSKI:def 4;

            hence x in (( L~ v) \/ ( LSeg (q1,p))) by XBOOLE_0:def 3;

          end;

        end;

        hence x in ( L~ f) & x in (( L~ v) \/ ( LSeg (q1,p)));

      end;

      thus ( L~ h) c= ( L~ f) by A127;

      

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

      thus ( L~ h) c= (( L~ (f | i)) \/ ( LSeg (q,p))) by A127;

      let x be object such that

       A143: x in (( L~ v) \/ ( LSeg (q,p)));

      now

        per cases by A143, XBOOLE_0:def 3;

          suppose x in ( L~ v);

          then

          consider X be set such that

           A144: x in X and

           A145: X in Mv by TARSKI:def 4;

          consider k such that

           A146: X = ( LSeg (v,k)) and

           A147: 1 <= k and

           A148: (k + 1) <= ( len v) by A145;

          

           A149: (k + 1) <= ( len h) by A26, A27, A142, A148, XXREAL_0: 2;

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

          then k <= ( len v) by A148, XXREAL_0: 2;

          then

           A150: k in ( Seg ( len v)) by A147, FINSEQ_1: 1;

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

          then (k + 1) in ( Seg ( len v)) by A148, FINSEQ_1: 1;

          then X = ( LSeg (h,k)) by A7, A126, A146, A150, TOPREAL3: 18;

          then X in Mh by A147, A149;

          hence thesis by A144, TARSKI:def 4;

        end;

          suppose

           A151: x in ( LSeg (q,p));

          ( LSeg (h,i)) in Mh by A4, A27;

          hence thesis by A31, A151, TARSKI:def 4;

        end;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL4:14

    

     Th14: (f /. 2) <> (f /. 1) & f is being_S-Seq & ((f /. 2) `2 ) = ((f /. 1) `2 ) & h = <*(f /. 1), |[((((f /. 1) `1 ) + ((f /. 2) `1 )) / 2), ((f /. 1) `2 )]|, (f /. 2)*> implies h is being_S-Seq & (h /. 1) = (f /. 1) & (h /. ( len h)) = (f /. 2) & ( L~ h) is_S-P_arc_joining ((f /. 1),(f /. 2)) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | 1)) \/ ( LSeg ((f /. 1),(f /. 2)))) & ( L~ h) = (( L~ (f | 2)) \/ ( LSeg ((f /. 2),(f /. 2))))

    proof

      set p1 = (f /. 1), p = (f /. 2);

      assume that

       A1: p <> p1 and

       A2: f is being_S-Seq and

       A3: (p `2 ) = (p1 `2 ) and

       A4: h = <*p1, |[(((p1 `1 ) + (p `1 )) / 2), (p1 `2 )]|, p*>;

      

       A5: (p1 `1 ) <> (p `1 ) by A1, A3, TOPREAL3: 6;

      hence

       A6: h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p by A3, A4, TOPREAL3: 37;

      

       A7: (( LSeg (p1, |[(((p1 `1 ) + (p `1 )) / 2), (p1 `2 )]|)) \/ ( LSeg ( |[(((p1 `1 ) + (p `1 )) / 2), (p1 `2 )]|,p))) = ( LSeg (p1,p)) by A3, A5, TOPREAL1: 5, TOPREAL3: 13;

      set M = { ( LSeg ((f | 2),k)) : 1 <= k & (k + 1) <= ( len (f | 2)) };

      

       A8: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      

       A9: ( L~ h) = (( LSeg (p1, |[(((p1 `1 ) + (p `1 )) / 2), (p1 `2 )]|)) \/ ( LSeg ( |[(((p1 `1 ) + (p `1 )) / 2), (p1 `2 )]|,p))) by A4, TOPREAL3: 16;

      

       A10: ( len f) >= 2 by A2;

      then

       A11: (1 + 1) in ( Seg ( len f)) by FINSEQ_1: 1;

      then

       A12: ( LSeg (f,1)) = ( LSeg (p1,p)) by A10, TOPREAL1:def 3;

      ( Seg 2) c= ( Seg ( len f)) by A10, FINSEQ_1: 5;

      then (f | 2) = (f | ( Seg 2)) & (( dom f) /\ ( Seg 2)) = ( Seg 2) by A8, FINSEQ_1:def 15, XBOOLE_1: 28;

      then

       A13: ( dom (f | 2)) = ( Seg 2) by RELAT_1: 61;

      then

       A14: 1 in ( dom (f | 2)) & 2 in ( dom (f | 2)) by FINSEQ_1: 1;

      thus

       A15: ( L~ h) is_S-P_arc_joining (p1,p) by A6;

      

       A16: (( L~ (f | 2)) \/ ( LSeg (p,p))) c= ( L~ h)

      proof

        let x be object such that

         A17: x in (( L~ (f | 2)) \/ ( LSeg (p,p)));

        now

          per cases by A17, XBOOLE_0:def 3;

            suppose x in ( L~ (f | 2));

            then

            consider X be set such that

             A18: x in X and

             A19: X in M by TARSKI:def 4;

            consider m such that

             A20: X = ( LSeg ((f | 2),m)) and

             A21: 1 <= m and

             A22: (m + 1) <= ( len (f | 2)) by A19;

            (( len (f | 2)) - 1) = ((1 + 1) - 1) by A13, FINSEQ_1:def 3

            .= 1;

            then ((m + 1) - 1) <= 1 by A22, XREAL_1: 9;

            then m = 1 by A21, XXREAL_0: 1;

            hence thesis by A11, A12, A9, A7, A14, A18, A20, TOPREAL3: 17;

          end;

            suppose x in ( LSeg (p,p));

            then

             A23: x in {p} by RLTOPSP1: 70;

            p in ( L~ h) by A15, Th3;

            hence thesis by A23, TARSKI:def 1;

          end;

        end;

        hence thesis;

      end;

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

      hence ( L~ h) c= ( L~ f) by A4, A12, A7, TOPREAL3: 16;

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

      then ( Seg 1) c= ( Seg ( len f)) by FINSEQ_1: 5;

      then (f | 1) = (f | ( Seg 1)) & (( dom f) /\ ( Seg 1)) = ( Seg 1) by A8, FINSEQ_1:def 15, XBOOLE_1: 28;

      then ( dom (f | 1)) = ( Seg 1) by RELAT_1: 61;

      then ( len (f | 1)) = 1 by FINSEQ_1:def 3;

      then ( L~ (f | 1)) = {} by TOPREAL1: 22;

      hence ( L~ h) = (( L~ (f | 1)) \/ ( LSeg (p1,p))) by A3, A5, A9, TOPREAL1: 5, TOPREAL3: 13;

      

       A24: ( L~ (f | 2)) c= (( L~ (f | 2)) \/ ( LSeg (p,p))) by XBOOLE_1: 7;

      

       A25: (1 + 1) <= ( len (f | 2)) by A13, FINSEQ_1:def 3;

      ( LSeg ((f | 2),1)) = ( LSeg (p1,p)) by A11, A12, A14, TOPREAL3: 17;

      then ( LSeg (p1,p)) in M by A25;

      then ( L~ h) c= ( L~ (f | 2)) by A9, A7, ZFMISC_1: 74;

      then ( L~ h) c= (( L~ (f | 2)) \/ ( LSeg (p,p))) by A24;

      hence thesis by A16;

    end;

    theorem :: TOPREAL4:15

    

     Th15: (f /. 2) <> (f /. 1) & f is being_S-Seq & ((f /. 2) `1 ) = ((f /. 1) `1 ) & h = <*(f /. 1), |[((f /. 1) `1 ), ((((f /. 1) `2 ) + ((f /. 2) `2 )) / 2)]|, (f /. 2)*> implies h is being_S-Seq & (h /. 1) = (f /. 1) & (h /. ( len h)) = (f /. 2) & ( L~ h) is_S-P_arc_joining ((f /. 1),(f /. 2)) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | 1)) \/ ( LSeg ((f /. 1),(f /. 2)))) & ( L~ h) = (( L~ (f | 2)) \/ ( LSeg ((f /. 2),(f /. 2))))

    proof

      set p1 = (f /. 1), p = (f /. 2);

      assume that

       A1: p <> p1 and

       A2: f is being_S-Seq and

       A3: (p `1 ) = (p1 `1 ) and

       A4: h = <*p1, |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|, p*>;

      

       A5: (p1 `2 ) <> (p `2 ) by A1, A3, TOPREAL3: 6;

      hence

       A6: h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p by A3, A4, TOPREAL3: 36;

      

       A7: (( LSeg (p1, |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|)) \/ ( LSeg ( |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|,p))) = ( LSeg (p1,p)) by A3, A5, TOPREAL1: 5, TOPREAL3: 14;

      set M = { ( LSeg ((f | 2),k)) : 1 <= k & (k + 1) <= ( len (f | 2)) };

      

       A8: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      

       A9: ( L~ h) = (( LSeg (p1, |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|)) \/ ( LSeg ( |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|,p))) by A4, TOPREAL3: 16;

      

       A10: ( len f) >= (1 + 1) by A2;

      then

       A11: ( LSeg (f,1)) = ( LSeg (p1,p)) by TOPREAL1:def 3;

      ( Seg 2) c= ( Seg ( len f)) by A10, FINSEQ_1: 5;

      then (f | 2) = (f | ( Seg 2)) & (( dom f) /\ ( Seg 2)) = ( Seg 2) by A8, FINSEQ_1:def 15, XBOOLE_1: 28;

      then

       A12: ( dom (f | 2)) = ( Seg 2) by RELAT_1: 61;

      then

       A13: 1 in ( dom (f | 2)) & 2 in ( dom (f | 2)) by FINSEQ_1: 1;

      thus

       A14: ( L~ h) is_S-P_arc_joining (p1,p) by A6;

      

       A15: (( L~ (f | 2)) \/ ( LSeg (p,p))) c= ( L~ h)

      proof

        let x be object such that

         A16: x in (( L~ (f | 2)) \/ ( LSeg (p,p)));

        now

          per cases by A16, XBOOLE_0:def 3;

            suppose x in ( L~ (f | 2));

            then

            consider X be set such that

             A17: x in X and

             A18: X in M by TARSKI:def 4;

            consider m such that

             A19: X = ( LSeg ((f | 2),m)) and

             A20: 1 <= m and

             A21: (m + 1) <= ( len (f | 2)) by A18;

            (( len (f | 2)) - 1) = ((1 + 1) - 1) by A12, FINSEQ_1:def 3

            .= 1;

            then ((m + 1) - 1) <= 1 by A21, XREAL_1: 9;

            then m = 1 by A20, XXREAL_0: 1;

            hence thesis by A10, A11, A9, A7, A13, A17, A19, TOPREAL3: 17;

          end;

            suppose x in ( LSeg (p,p));

            then

             A22: x in {p} by RLTOPSP1: 70;

            p in ( L~ h) by A14, Th3;

            hence thesis by A22, TARSKI:def 1;

          end;

        end;

        hence thesis;

      end;

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

      hence ( L~ h) c= ( L~ f) by A4, A11, A7, TOPREAL3: 16;

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

      then ( Seg 1) c= ( Seg ( len f)) by FINSEQ_1: 5;

      then (f | 1) = (f | ( Seg 1)) & (( dom f) /\ ( Seg 1)) = ( Seg 1) by A8, FINSEQ_1:def 15, XBOOLE_1: 28;

      then ( dom (f | 1)) = ( Seg 1) by RELAT_1: 61;

      then ( len (f | 1)) = 1 by FINSEQ_1:def 3;

      then ( L~ (f | 1)) = {} by TOPREAL1: 22;

      hence ( L~ h) = (( L~ (f | 1)) \/ ( LSeg (p1,p))) by A3, A5, A9, TOPREAL1: 5, TOPREAL3: 14;

      

       A23: ( L~ (f | 2)) c= (( L~ (f | 2)) \/ ( LSeg (p,p))) by XBOOLE_1: 7;

      

       A24: (1 + 1) <= ( len (f | 2)) by A12, FINSEQ_1:def 3;

      ( LSeg ((f | 2),1)) = ( LSeg (p1,p)) by A10, A11, A13, TOPREAL3: 17;

      then ( LSeg (p1,p)) in M by A24;

      then ( L~ h) c= ( L~ (f | 2)) by A9, A7, ZFMISC_1: 74;

      then ( L~ h) c= (( L~ (f | 2)) \/ ( LSeg (p,p))) by A23;

      hence thesis by A15;

    end;

    theorem :: TOPREAL4:16

    

     Th16: f is being_S-Seq & i > 2 & i in ( dom f) & h = (f | i) implies h is being_S-Seq & (h /. 1) = (f /. 1) & (h /. ( len h)) = (f /. i) & ( L~ h) is_S-P_arc_joining ((f /. 1),(f /. i)) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | i)) \/ ( LSeg ((f /. i),(f /. i))))

    proof

      assume that

       A1: f is being_S-Seq & i > 2 and

       A2: i in ( dom f) and

       A3: h = (f | i);

      

       A4: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      then i <= ( len f) by A2, FINSEQ_1: 1;

      then

       A5: ( Seg i) c= ( Seg ( len f)) by FINSEQ_1: 5;

      h = (f | ( Seg i)) by A3, FINSEQ_1:def 15;

      then ( dom h) = (( Seg ( len f)) /\ ( Seg i)) by A4, RELAT_1: 61;

      then

       A6: ( dom h) = ( Seg i) by A5, XBOOLE_1: 28;

      1 <= i by A2, A4, FINSEQ_1: 1;

      then

       A7: 1 in ( dom h) & i in ( dom h) by A6, FINSEQ_1: 1;

      i in NAT by ORDINAL1:def 12;

      then ( len h) = i by A6, FINSEQ_1:def 3;

      hence h is being_S-Seq & (h /. 1) = (f /. 1) & (h /. ( len h)) = (f /. i) by A1, A2, A3, A7, FINSEQ_4: 70, TOPREAL3: 33;

      hence ( L~ h) is_S-P_arc_joining ((f /. 1),(f /. i)) & ( L~ h) c= ( L~ f) by A3, TOPREAL3: 20;

      then (f /. i) in ( L~ (f | i)) by A3, Th3;

      then ( LSeg ((f /. i),(f /. i))) = {(f /. i)} & {(f /. i)} c= ( L~ (f | i)) by RLTOPSP1: 70, ZFMISC_1: 31;

      hence thesis by A3, XBOOLE_1: 12;

    end;

    theorem :: TOPREAL4:17

    

     Th17: p <> (f /. 1) & f is being_S-Seq & p in ( LSeg (f,n)) implies ex h st h is being_S-Seq & (h /. 1) = (f /. 1) & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining ((f /. 1),p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | n)) \/ ( LSeg ((f /. n),p)))

    proof

      set p1 = (f /. 1), q = (f /. n);

      assume that

       A1: p <> p1 and

       A2: f is being_S-Seq and

       A3: p in ( LSeg (f,n));

      

       A4: f is special by A2;

      

       A5: n <= (n + 1) by NAT_1: 11;

       A6:

      now

        assume

         A7: not n in ( dom f) or not (n + 1) in ( dom f);

        now

          per cases by A7;

            suppose not n in ( dom f);

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

            then not (1 <= n & (n + 1) <= ( len f)) by A5, XXREAL_0: 2;

            hence contradiction by A3, TOPREAL1:def 3;

          end;

            suppose not (n + 1) in ( dom f);

            then not (1 <= (n + 1) & (n + 1) <= ( len f)) by FINSEQ_3: 25;

            hence contradiction by A3, NAT_1: 11, TOPREAL1:def 3;

          end;

        end;

        hence contradiction;

      end;

      

       A8: f is one-to-one by A2;

      

       A9: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      then

       A10: 1 <= n by A6, FINSEQ_1: 1;

      

       A11: (n + 1) <= ( len f) by A6, A9, FINSEQ_1: 1;

      

       A12: n <= ( len f) by A6, A9, FINSEQ_1: 1;

      now

        per cases ;

          case (f /. n) = p & (f /. (n + 1)) = p;

          then (n + 1) = n by A6, A8, PARTFUN2: 10;

          hence contradiction;

        end;

          case

           A13: (f /. n) = p & (f /. (n + 1)) <> p;

          then 1 < n by A1, A10, XXREAL_0: 1;

          then

           A14: (1 + 1) <= n by NAT_1: 13;

          now

            per cases by A14, XXREAL_0: 1;

              suppose

               A15: n = (1 + 1);

              now

                per cases by A4, A12, A13, A15;

                  suppose

                   A16: (p1 `1 ) = (p `1 );

                  take h = <*p1, |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|, p*>;

                  thus h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining (p1,p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | n)) \/ ( LSeg (q,p))) by A1, A2, A13, A15, A16, Th15;

                end;

                  suppose

                   A17: (p1 `2 ) = (p `2 );

                  take h = <*p1, |[(((p1 `1 ) + (p `1 )) / 2), (p1 `2 )]|, p*>;

                  thus h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining (p1,p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | n)) \/ ( LSeg (q,p))) by A1, A2, A13, A15, A17, Th14;

                end;

              end;

              hence thesis;

            end;

              suppose

               A18: n > 2;

              take h = (f | n);

              thus h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining (p1,p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | n)) \/ ( LSeg (q,p))) by A2, A6, A13, A18, Th16;

            end;

          end;

          hence thesis;

        end;

          case

           A19: (f /. n) <> p & (f /. (n + 1)) = p;

          now

            per cases by A10, XXREAL_0: 1;

              suppose

               A20: n = 1;

              now

                per cases by A4, A11, A19, A20;

                  suppose

                   A21: (p1 `1 ) = (p `1 );

                  take h = <*p1, |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|, p*>;

                  thus h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining (p1,p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | n)) \/ ( LSeg (q,p))) by A2, A19, A20, A21, Th15;

                end;

                  suppose

                   A22: (p1 `2 ) = (p `2 );

                  take h = <*p1, |[(((p1 `1 ) + (p `1 )) / 2), (p1 `2 )]|, p*>;

                  thus h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining (p1,p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | n)) \/ ( LSeg (q,p))) by A2, A19, A20, A22, Th14;

                end;

              end;

              hence thesis;

            end;

              suppose

               A23: 1 < n;

              take h = (f | (n + 1));

              (1 + 1) < (n + 1) by A23, XREAL_1: 6;

              hence h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining (p1,p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | n)) \/ ( LSeg (q,p))) by A2, A6, A19, Th16, TOPREAL3: 38;

            end;

          end;

          hence thesis;

        end;

          case

           A24: (f /. n) <> p & (f /. (n + 1)) <> p;

          now

            per cases by A10, XXREAL_0: 1;

              suppose

               A25: n = 1;

              set q1 = (f /. (1 + 1));

              

               A26: ( len f) >= (1 + 1) by A2;

              then

               A27: ( LSeg (f,n)) = ( LSeg (p1,q1)) by A25, TOPREAL1:def 3;

              now

                per cases by A4, A26;

                  suppose

                   A28: (p1 `1 ) = (q1 `1 );

                  take h = <*p1, |[(p1 `1 ), (((p1 `2 ) + (p `2 )) / 2)]|, p*>;

                  (p1 `1 ) <= (p `1 ) & (p `1 ) <= (q1 `1 ) by A3, A27, A28, TOPREAL1: 3;

                  then (p1 `1 ) = (p `1 ) by A28, XXREAL_0: 1;

                  hence h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining (p1,p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | n)) \/ ( LSeg (q,p))) by A1, A2, A3, A25, Th12;

                end;

                  suppose

                   A29: (p1 `2 ) = (q1 `2 );

                  take h = <*p1, |[(((p1 `1 ) + (p `1 )) / 2), (p1 `2 )]|, p*>;

                  (p1 `2 ) <= (p `2 ) & (p `2 ) <= (q1 `2 ) by A3, A27, A29, TOPREAL1: 4;

                  then (p1 `2 ) = (p `2 ) by A29, XXREAL_0: 1;

                  hence h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining (p1,p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | n)) \/ ( LSeg (q,p))) by A1, A2, A3, A25, Th11;

                end;

              end;

              hence thesis;

            end;

              suppose

               A30: 1 < n;

              take h = ((f | n) ^ <*p*>);

              thus h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining (p1,p) & ( L~ h) c= ( L~ f) & ( L~ h) = (( L~ (f | n)) \/ ( LSeg (q,p))) by A2, A3, A6, A24, A30, Th13;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL4:18

    

     Th18: p <> (f /. 1) & f is being_S-Seq & p in ( L~ f) implies ex h st h is being_S-Seq & (h /. 1) = (f /. 1) & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining ((f /. 1),p) & ( L~ h) c= ( L~ f)

    proof

      set M = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) }, p1 = (f /. 1);

      assume that

       A1: p <> p1 & f is being_S-Seq and

       A2: p in ( L~ f);

      consider X be set such that

       A3: p in X and

       A4: X in M by A2, TARSKI:def 4;

      consider n such that

       A5: X = ( LSeg (f,n)) and 1 <= n and (n + 1) <= ( len f) by A4;

      consider h such that

       A6: h is being_S-Seq & (h /. 1) = p1 & (h /. ( len h)) = p & ( L~ h) is_S-P_arc_joining (p1,p) & ( L~ h) c= ( L~ f) and ( L~ h) = (( L~ (f | n)) \/ ( LSeg ((f /. n),p))) by A1, A3, A5, Th17;

      take h;

      thus thesis by A6;

    end;

    theorem :: TOPREAL4:19

    

     Th19: ((p `1 ) = ((f /. ( len f)) `1 ) & (p `2 ) <> ((f /. ( len f)) `2 ) or (p `1 ) <> ((f /. ( len f)) `1 ) & (p `2 ) = ((f /. ( len f)) `2 )) & (f /. ( len f)) in ( Ball (u,r)) & p in ( Ball (u,r)) & f is being_S-Seq & (( LSeg ((f /. ( len f)),p)) /\ ( L~ f)) = {(f /. ( len f))} & h = (f ^ <*p*>) implies h is being_S-Seq & ( L~ h) is_S-P_arc_joining ((f /. 1),p) & ( L~ h) c= (( L~ f) \/ ( Ball (u,r)))

    proof

      set p1 = (f /. 1), p2 = (f /. ( len f));

      assume

       A1: (p `1 ) = (p2 `1 ) & (p `2 ) <> (p2 `2 ) or (p `1 ) <> (p2 `1 ) & (p `2 ) = (p2 `2 );

      assume that

       A2: p2 in ( Ball (u,r)) & p in ( Ball (u,r)) and

       A3: f is being_S-Seq and

       A4: (( LSeg (p2,p)) /\ ( L~ f)) = {p2} and

       A5: h = (f ^ <*p*>);

      

       A6: not p in ( L~ f) by A1, A4, TOPREAL3: 40;

      

       A7: f is one-to-one by A3;

      

       A8: f is unfolded by A3;

      

       A9: f is one-to-one by A3;

      

       A10: f is s.n.c. by A3;

      

       A11: ( Seg ( len h)) = ( dom h) by FINSEQ_1:def 3;

      set Mf = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) }, Mh = { ( LSeg (h,m)) : 1 <= m & (m + 1) <= ( len h) };

      

       A12: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      

       A13: 2 <= ( len f) by A3;

      then

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

      then

       A15: ( len f) in ( dom f) by A12, FINSEQ_1: 1;

      then

       A16: (h /. ( len f)) = p2 by A5, FINSEQ_4: 68;

      

       A17: ( len h) = (( len f) + ( len <*p*>)) by A5, FINSEQ_1: 22

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

      then

       A18: (h /. ( len h)) = p by A5, FINSEQ_4: 67;

      then

       A19: ( LSeg (h,( len f))) = ( LSeg (p2,p)) by A17, A14, A16, TOPREAL1:def 3;

      

       A20: f is special by A3;

      thus

       A21: h is being_S-Seq

      proof

        now

          set Z = { m where m be Nat : 1 <= m & m <= ( len h) };

          given x,y be object such that

           A22: x in ( dom h) and

           A23: y in ( dom h) and

           A24: (h . x) = (h . y) and

           A25: x <> y;

          y in Z by A11, A23, FINSEQ_1:def 1;

          then

          consider k2 be Nat such that

           A26: k2 = y and

           A27: 1 <= k2 and

           A28: k2 <= ( len h);

          x in Z by A11, A22, FINSEQ_1:def 1;

          then

          consider k1 be Nat such that

           A29: k1 = x and

           A30: 1 <= k1 and

           A31: k1 <= ( len h);

          

           A32: (h /. k1) = (h . y) by A22, A24, A29, PARTFUN1:def 6

          .= (h /. k2) by A23, A26, PARTFUN1:def 6;

          now

            per cases by A17, A31, A28, XXREAL_0: 1;

              suppose k1 = (( len f) + 1) & k2 = (( len f) + 1);

              hence contradiction by A25, A29, A26;

            end;

              suppose

               A33: k1 = (( len f) + 1) & k2 < (( len f) + 1);

              then

               A34: (k2 + 1) <= k1 by NAT_1: 13;

              now

                per cases by A34, XXREAL_0: 1;

                  suppose (k2 + 1) = k1;

                  hence contradiction by A1, A5, A16, A32, A33, FINSEQ_4: 67;

                end;

                  suppose (k2 + 1) < k1;

                  then

                   A35: k2 < ((( len f) + 1) - 1) by A33, XREAL_1: 20;

                  reconsider k2 as Element of NAT by ORDINAL1:def 12;

                  k2 in ( dom f) by A12, A27, A35, FINSEQ_1: 1;

                  then (h /. k2) = (f /. k2) by A5, FINSEQ_4: 68;

                  hence contradiction by A5, A13, A6, A27, A32, A33, A35, FINSEQ_4: 67, TOPREAL3: 39;

                end;

              end;

              hence contradiction;

            end;

              suppose

               A36: k1 < (( len f) + 1) & k2 = (( len f) + 1);

              then

               A37: (k1 + 1) <= k2 by NAT_1: 13;

              now

                per cases by A37, XXREAL_0: 1;

                  suppose (k1 + 1) = k2;

                  hence contradiction by A1, A5, A16, A32, A36, FINSEQ_4: 67;

                end;

                  suppose (k1 + 1) < k2;

                  then

                   A38: k1 < ((( len f) + 1) - 1) by A36, XREAL_1: 20;

                  reconsider k1 as Element of NAT by ORDINAL1:def 12;

                  k1 in ( dom f) by A12, A30, A38, FINSEQ_1: 1;

                  then (h /. k1) = (f /. k1) by A5, FINSEQ_4: 68;

                  hence contradiction by A5, A13, A6, A30, A32, A36, A38, FINSEQ_4: 67, TOPREAL3: 39;

                end;

              end;

              hence contradiction;

            end;

              suppose

               A39: k1 < (( len f) + 1) & k2 < (( len f) + 1);

              then k2 <= ( len f) by NAT_1: 13;

              then

               A40: k2 in ( dom f) by A12, A27, FINSEQ_1: 1;

              k1 <= ( len f) by A39, NAT_1: 13;

              then

               A41: k1 in ( dom f) by A12, A30, FINSEQ_1: 1;

              

              then (f . k1) = (h . k1) by A5, FINSEQ_1:def 7

              .= (f . k2) by A5, A24, A29, A26, A40, FINSEQ_1:def 7;

              hence contradiction by A9, A25, A29, A26, A41, A40, FUNCT_1:def 4;

            end;

          end;

          hence contradiction;

        end;

        hence h is one-to-one by FUNCT_1:def 4;

        (2 + 1) <= (( len f) + 1) by A13, XREAL_1: 6;

        hence ( len h) >= 2 by A17, XXREAL_0: 2;

        thus h is unfolded

        proof

          let j be Nat such that

           A42: 1 <= j and

           A43: (j + 2) <= ( len h);

          

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

          (j + 1) <= (j + 2) by XREAL_1: 6;

          then

           A45: (j + 1) <= ( len h) by A43, XXREAL_0: 2;

          now

            per cases by A43, XXREAL_0: 1;

              suppose

               A46: (j + 2) = ( len h);

              then

               A47: (j + ((1 + 1) - 1)) = ( len f) by A17;

              then j <= ( len f) by NAT_1: 13;

              then j in ( dom f) by A12, A42, FINSEQ_1: 1;

              then

               A48: ( LSeg (h,j)) = ( LSeg (f,j)) by A5, A15, A47, TOPREAL3: 18;

              ( LSeg (h,j)) in Mf by A42, A47, A48;

              then

               A49: ( LSeg (h,j)) = (( LSeg (h,j)) /\ ( L~ f)) by XBOOLE_1: 28, ZFMISC_1: 74;

              (h /. (j + 1)) in ( LSeg (h,j)) by A42, A45, TOPREAL1: 21;

              then

               A50: {(h /. (j + 1))} c= ( LSeg (h,j)) by ZFMISC_1: 31;

              ( LSeg (h,(j + 1))) = ( LSeg (p2,p)) by A17, A14, A18, A16, A46, TOPREAL1:def 3;

              

              hence (( LSeg (h,j)) /\ ( LSeg (h,(j + 1)))) = (( LSeg (h,j)) /\ {(h /. (j + 1))}) by A4, A17, A16, A46, A49, XBOOLE_1: 16

              .= {(h /. (j + 1))} by A50, XBOOLE_1: 28;

            end;

              suppose (j + 2) < ( len h);

              then

               A51: ((j + (2 + 1)) - 1) <= ( len f) by A17, NAT_1: 13;

              then

               A52: (( LSeg (f,j)) /\ ( LSeg (f,(j + 1)))) = {(f /. (j + 1))} by A8, A42, A43;

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

              then

               A53: ((j + 1) + 1) in ( dom f) by A12, A51, FINSEQ_1: 1;

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

              then

               A54: (j + 1) <= ( len f) by A51, XXREAL_0: 2;

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

              then

               A55: (j + 1) in ( dom f) by A12, A54, FINSEQ_1: 1;

              then

               A56: (h /. (j + 1)) = (f /. (j + 1)) by A5, FINSEQ_4: 68;

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

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

              then j in ( dom f) by A12, A42, FINSEQ_1: 1;

              then ( LSeg (h,j)) = ( LSeg (f,j)) by A5, A55, TOPREAL3: 18;

              hence thesis by A5, A52, A55, A53, A56, TOPREAL3: 18;

            end;

          end;

          hence thesis;

        end;

        thus h is s.n.c.

        proof

          let n,m be Nat such that

           A57: m > (n + 1);

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

          then

           A58: n <= m by A57, XXREAL_0: 2;

          

           A59: ((n + 1) + 1) = (n + (1 + 1));

          

           A60: 1 <= (n + 1) by NAT_1: 11;

          ( LSeg (f,n)) misses ( LSeg (f,m)) by A10, A57;

          then

           A61: (( LSeg (f,n)) /\ ( LSeg (f,m))) = {} ;

          now

            per cases by XXREAL_0: 1;

              suppose

               A62: (m + 1) < ( len h);

              then

               A63: (m + 1) <= ( len f) by A17, NAT_1: 13;

              

               A64: 1 < m by A57, A60, XXREAL_0: 2;

              then 1 <= (m + 1) by NAT_1: 13;

              then

               A65: (m + 1) in ( dom f) by A12, A63, FINSEQ_1: 1;

              

               A66: m <= ( len f) by A17, A62, XREAL_1: 6;

              then m in ( dom f) by A12, A64, FINSEQ_1: 1;

              then

               A67: ( LSeg (h,m)) = ( LSeg (f,m)) by A5, A65, TOPREAL3: 18;

              now

                per cases ;

                  suppose 0 < n;

                  then

                   A68: ( 0 + 1) <= n by NAT_1: 13;

                  (n + 1) <= ( len f) by A57, A66, XXREAL_0: 2;

                  then

                   A69: (n + 1) in ( dom f) by A12, A60, FINSEQ_1: 1;

                  n <= ( len f) by A58, A66, XXREAL_0: 2;

                  then n in ( dom f) by A12, A68, FINSEQ_1: 1;

                  hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} by A5, A61, A67, A69, TOPREAL3: 18;

                end;

                  suppose 0 = n;

                  then ( LSeg (h,n)) = {} by TOPREAL1:def 3;

                  hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

                end;

              end;

              hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

            end;

              suppose

               A70: (m + 1) = ( len h);

              now

                per cases ;

                  suppose

                   A71: 0 < n;

                  

                   A72: (n + 1) in ( dom f) by A17, A12, A57, A60, A70, FINSEQ_1: 1;

                  

                   A73: ( 0 + 1) <= n by A71, NAT_1: 13;

                  then n in ( dom f) by A17, A12, A58, A70, FINSEQ_1: 1;

                  then

                   A74: ( LSeg (h,n)) = ( LSeg (f,n)) by A5, A72, TOPREAL3: 18;

                  now

                    set L = ( LSeg (f,n));

                    set x = the Element of (( LSeg (h,n)) /\ ( LSeg (h,m)));

                    assume

                     A75: (( LSeg (h,n)) /\ ( LSeg (h,m))) <> {} ;

                    then

                     A76: x in L by A74, XBOOLE_0:def 4;

                    

                     A77: x in ( LSeg (p2,p)) by A17, A19, A70, A75, XBOOLE_0:def 4;

                    L in Mf by A17, A57, A70, A73;

                    then x in ( L~ f) by A76, TARSKI:def 4;

                    then x in {p2} by A4, A77, XBOOLE_0:def 4;

                    then

                     A78: x = p2 by TARSKI:def 1;

                    

                     A79: ((n + 1) + 1) <= ( len f) by A17, A57, A70, NAT_1: 13;

                    now

                      per cases by A79, XXREAL_0: 1;

                        suppose

                         A80: ((n + 1) + 1) = ( len f);

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

                        then

                         A81: p2 in ( LSeg (f,(n + 1))) by A80, TOPREAL1: 21;

                        (( LSeg (f,n)) /\ ( LSeg (f,(n + 1)))) = {(f /. (n + 1))} by A8, A59, A73, A80;

                        then p2 in {(f /. (n + 1))} by A76, A78, A81, XBOOLE_0:def 4;

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

                        then (( len f) + 1) = ( len f) by A15, A7, A72, A80, PARTFUN2: 10;

                        hence contradiction;

                      end;

                        suppose

                         A82: ((n + 1) + 1) < ( len f);

                        reconsider j = (( len f) - 1) as Element of NAT by A13, INT_1: 5, XXREAL_0: 2;

                        ((n + 2) + 1) <= ( len f) by A82, NAT_1: 13;

                        then (n + 2) <= (( len f) - 1) by XREAL_1: 19;

                        then (n + 1) < j by A59, NAT_1: 13;

                        then ( LSeg (f,n)) misses ( LSeg (f,j)) by A10;

                        then

                         A83: (( LSeg (f,n)) /\ ( LSeg (f,j))) = {} ;

                        ((1 + 1) - 1) = 1;

                        then (j + 1) = ( len f) & 1 <= j by A13, XREAL_1: 13;

                        then p2 in ( LSeg (f,j)) by TOPREAL1: 21;

                        hence contradiction by A76, A78, A83, XBOOLE_0:def 4;

                      end;

                    end;

                    hence contradiction;

                  end;

                  hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

                end;

                  suppose 0 = n;

                  then ( LSeg (h,n)) = {} by TOPREAL1:def 3;

                  hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

                end;

              end;

              hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

            end;

              suppose (m + 1) > ( len h);

              then ( LSeg (h,m)) = {} by TOPREAL1:def 3;

              hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

            end;

          end;

          hence (( LSeg (h,n)) /\ ( LSeg (h,m))) = {} ;

        end;

        hereby

          let n be Nat such that

           A84: 1 <= n and

           A85: (n + 1) <= ( len h);

          set p3 = (h /. n), p4 = (h /. (n + 1));

          now

            per cases by A85, XXREAL_0: 1;

              suppose (n + 1) = ( len h);

              hence (p3 `1 ) = (p4 `1 ) or (p3 `2 ) = (p4 `2 ) by A1, A5, A17, A16, FINSEQ_4: 67;

            end;

              suppose

               A86: (n + 1) < ( len h);

              

               A87: 1 <= (n + 1) by A84, NAT_1: 13;

              (n + 1) <= ( len f) by A17, A86, NAT_1: 13;

              then (n + 1) in ( dom f) by A12, A87, FINSEQ_1: 1;

              then

               A88: p4 = (f /. (n + 1)) by A5, FINSEQ_4: 68;

              n <= ( len f) by A17, A86, XREAL_1: 6;

              then n in ( dom f) by A12, A84, FINSEQ_1: 1;

              then

               A89: p3 = (f /. n) by A5, FINSEQ_4: 68;

              (n + 1) <= ( len f) by A17, A86, NAT_1: 13;

              hence (p3 `1 ) = (p4 `1 ) or (p3 `2 ) = (p4 `2 ) by A20, A84, A89, A88;

            end;

          end;

          hence (p3 `1 ) = (p4 `1 ) or (p3 `2 ) = (p4 `2 );

        end;

      end;

      1 in ( dom f) by A12, A14, FINSEQ_1: 1;

      then (h /. 1) = p1 by A5, FINSEQ_4: 68;

      hence ( L~ h) is_S-P_arc_joining (p1,p) by A18, A21;

      let x be object;

      assume x in ( L~ h);

      then

      consider X be set such that

       A90: x in X and

       A91: X in Mh by TARSKI:def 4;

      consider k such that

       A92: X = ( LSeg (h,k)) and

       A93: 1 <= k and

       A94: (k + 1) <= ( len h) by A91;

      per cases by A94, XXREAL_0: 1;

        suppose

         A95: (k + 1) = ( len h);

        

         A96: ( Ball (u,r)) c= (( L~ f) \/ ( Ball (u,r))) by XBOOLE_1: 7;

        X c= ( Ball (u,r)) by A2, A17, A19, A92, A95, TOPREAL3: 21;

        hence thesis by A90, A96;

      end;

        suppose (k + 1) < ( len h);

        then

         A97: (k + 1) <= ( len f) by A17, NAT_1: 13;

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

        then k <= ( len f) by A97, XXREAL_0: 2;

        then

         A98: k in ( dom f) by A12, A93, FINSEQ_1: 1;

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

        then (k + 1) in ( dom f) by A12, A97, FINSEQ_1: 1;

        then X = ( LSeg (f,k)) by A5, A92, A98, TOPREAL3: 18;

        then X in Mf by A93, A97;

        then x in ( union Mf) by A90, TARSKI:def 4;

        hence thesis by XBOOLE_0:def 3;

      end;

    end;

    theorem :: TOPREAL4:20

    

     Th20: (f /. ( len f)) in ( Ball (u,r)) & p in ( Ball (u,r)) & |[(p `1 ), ((f /. ( len f)) `2 )]| in ( Ball (u,r)) & f is being_S-Seq & (p `1 ) <> ((f /. ( len f)) `1 ) & (p `2 ) <> ((f /. ( len f)) `2 ) & h = (f ^ <* |[(p `1 ), ((f /. ( len f)) `2 )]|, p*>) & ((( LSeg ((f /. ( len f)), |[(p `1 ), ((f /. ( len f)) `2 )]|)) \/ ( LSeg ( |[(p `1 ), ((f /. ( len f)) `2 )]|,p))) /\ ( L~ f)) = {(f /. ( len f))} implies ( L~ h) is_S-P_arc_joining ((f /. 1),p) & ( L~ h) c= (( L~ f) \/ ( Ball (u,r)))

    proof

      set p1 = (f /. 1), p2 = (f /. ( len f));

      assume that

       A1: p2 in ( Ball (u,r)) and

       A2: p in ( Ball (u,r)) and

       A3: |[(p `1 ), (p2 `2 )]| in ( Ball (u,r)) and

       A4: f is being_S-Seq and

       A5: (p `1 ) <> (p2 `1 ) and

       A6: (p `2 ) <> (p2 `2 ) and

       A7: h = (f ^ <* |[(p `1 ), (p2 `2 )]|, p*>) and

       A8: ((( LSeg (p2, |[(p `1 ), (p2 `2 )]|)) \/ ( LSeg ( |[(p `1 ), (p2 `2 )]|,p))) /\ ( L~ f)) = {p2};

      set p3 = |[(p `1 ), (p2 `2 )]|, f1 = (f ^ <*p3*>), h1 = (f1 ^ <*p*>);

      reconsider Lf = ( L~ f) as non empty Subset of ( TOP-REAL 2) by A8;

      

       A9: p2 in ( LSeg (p2,p3)) by RLTOPSP1: 68;

      ( L~ f) is_S-P_arc_joining (p1,p2) by A4;

      then Lf is_an_arc_of (p1,p2) by Th2;

      then p2 in ( L~ f) by TOPREAL1: 1;

      then p2 in (( LSeg (p2,p3)) /\ ( L~ f)) by A9, XBOOLE_0:def 4;

      then

       A10: (( LSeg (p2,p3)) /\ ( L~ f)) c= ((( LSeg (p2,p3)) /\ ( L~ f)) \/ (( LSeg (p3,p)) /\ ( L~ f))) & {p2} c= (( LSeg (p2,p3)) /\ ( L~ f)) by XBOOLE_1: 7, ZFMISC_1: 31;

       {p2} = ((( LSeg (p2,p3)) /\ ( L~ f)) \/ (( LSeg (p3,p)) /\ ( L~ f))) by A8, XBOOLE_1: 23;

      then

       A11: (( LSeg (p2,p3)) /\ ( L~ f)) = {p2} by A10;

      

       A12: ( len f1) = (( len f) + ( len <*p3*>)) by FINSEQ_1: 22

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

      then

       A13: (f1 /. ( len f1)) = p3 by FINSEQ_4: 67;

      

       A14: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

       A15: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      ( len f) >= 2 by A4;

      then

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

      then ( len f) in ( dom f) by A15, FINSEQ_1: 1;

      then

       A17: (f1 /. ( len f)) = p2 by FINSEQ_4: 68;

      

       A18: (( LSeg (p3,p)) /\ ( L~ f1)) c= {p3}

      proof

        set M1 = { ( LSeg (f1,i)) : 1 <= i & (i + 1) <= ( len f1) }, Mf = { ( LSeg (f,j)) : 1 <= j & (j + 1) <= ( len f) };

        assume not thesis;

        then

        consider x be object such that

         A19: x in (( LSeg (p3,p)) /\ ( L~ f1)) and

         A20: not x in {p3};

        x in ( L~ f1) by A19, XBOOLE_0:def 4;

        then

        consider X be set such that

         A21: x in X and

         A22: X in M1 by TARSKI:def 4;

        consider k such that

         A23: X = ( LSeg (f1,k)) and

         A24: 1 <= k and

         A25: (k + 1) <= ( len f1) by A22;

        

         A26: x in ( LSeg (p3,p)) by A19, XBOOLE_0:def 4;

        now

          per cases by A25, XXREAL_0: 1;

            suppose (k + 1) = ( len f1);

            then ( LSeg (f1,k)) = ( LSeg (p2,p3)) by A12, A13, A17, A24, TOPREAL1:def 3;

            then x in (( LSeg (p2,p3)) /\ ( LSeg (p3,p))) by A26, A21, A23, XBOOLE_0:def 4;

            hence contradiction by A20, TOPREAL3: 30;

          end;

            suppose (k + 1) < ( len f1);

            then

             A27: (k + 1) <= ( len f) by A12, NAT_1: 13;

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

            then k <= ( len f) by A27, XXREAL_0: 2;

            then

             A28: k in ( dom f) by A15, A24, FINSEQ_1: 1;

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

            then (k + 1) in ( dom f) by A15, A27, FINSEQ_1: 1;

            then X = ( LSeg (f,k)) by A23, A28, TOPREAL3: 18;

            then X in Mf by A24, A27;

            then

             A29: x in ( L~ f) by A21, TARSKI:def 4;

            x in (( LSeg (p2,p3)) \/ ( LSeg (p3,p))) by A26, XBOOLE_0:def 3;

            then x in {p2} by A8, A29, XBOOLE_0:def 4;

            then x = p2 by TARSKI:def 1;

            hence contradiction by A5, A14, A26, TOPREAL3: 11;

          end;

        end;

        hence contradiction;

      end;

      

       A30: h1 = (f ^ ( <*p3*> ^ <*p*>)) by FINSEQ_1: 32

      .= h by A7, FINSEQ_1:def 9;

      

       A31: (p3 `2 ) = (p2 `2 ) & (p3 `1 ) = (p `1 ) by EUCLID: 52;

      then

       A32: f1 is being_S-Seq by A1, A3, A4, A5, A11, Th19;

      

       A33: ( L~ f1) is_S-P_arc_joining (p1,p3) by A1, A3, A4, A5, A31, A11, Th19;

      then

      reconsider Lf1 = ( L~ f1) as non empty Subset of ( TOP-REAL 2) by Th1, TOPREAL1: 26;

      

       A34: p3 in ( LSeg (p3,p)) by RLTOPSP1: 68;

      

       A35: (f1 /. ( len f1)) = p3 by A12, FINSEQ_4: 67;

      ( L~ f1) c= (( L~ f) \/ ( Ball (u,r))) by A1, A3, A4, A5, A31, A11, Th19;

      then (( L~ f1) \/ ( Ball (u,r))) c= ((( L~ f) \/ ( Ball (u,r))) \/ ( Ball (u,r))) by XBOOLE_1: 9;

      then

       A36: (( L~ f1) \/ ( Ball (u,r))) c= (( L~ f) \/ (( Ball (u,r)) \/ ( Ball (u,r)))) by XBOOLE_1: 4;

      

       A37: (p `1 ) = (p3 `1 ) & (p `2 ) <> (p3 `2 ) or (p `1 ) <> (p3 `1 ) & (p `2 ) = (p3 `2 ) by A6, EUCLID: 52;

      Lf1 is_an_arc_of (p1,p3) by A33, Th2;

      then p3 in ( L~ f1) by TOPREAL1: 1;

      then p3 in (( LSeg (p3,p)) /\ ( L~ f1)) by A34, XBOOLE_0:def 4;

      then {p3} c= (( LSeg (p3,p)) /\ ( L~ f1)) by ZFMISC_1: 31;

      then

       A38: (( LSeg (p3,p)) /\ ( L~ f1)) = {p3} by A18;

      1 in ( dom f) by A15, A16, FINSEQ_1: 1;

      then (f1 /. 1) = p1 by FINSEQ_4: 68;

      hence ( L~ h) is_S-P_arc_joining (p1,p) by A2, A3, A37, A32, A35, A38, A30, Th19;

      ( L~ h1) c= (( L~ f1) \/ ( Ball (u,r))) by A2, A3, A37, A32, A35, A38, Th19;

      hence thesis by A30, A36;

    end;

    theorem :: TOPREAL4:21

    

     Th21: (f /. ( len f)) in ( Ball (u,r)) & p in ( Ball (u,r)) & |[((f /. ( len f)) `1 ), (p `2 )]| in ( Ball (u,r)) & f is being_S-Seq & (p `1 ) <> ((f /. ( len f)) `1 ) & (p `2 ) <> ((f /. ( len f)) `2 ) & h = (f ^ <* |[((f /. ( len f)) `1 ), (p `2 )]|, p*>) & ((( LSeg ((f /. ( len f)), |[((f /. ( len f)) `1 ), (p `2 )]|)) \/ ( LSeg ( |[((f /. ( len f)) `1 ), (p `2 )]|,p))) /\ ( L~ f)) = {(f /. ( len f))} implies ( L~ h) is_S-P_arc_joining ((f /. 1),p) & ( L~ h) c= (( L~ f) \/ ( Ball (u,r)))

    proof

      set p1 = (f /. 1), p2 = (f /. ( len f));

      assume that

       A1: p2 in ( Ball (u,r)) and

       A2: p in ( Ball (u,r)) and

       A3: |[(p2 `1 ), (p `2 )]| in ( Ball (u,r)) and

       A4: f is being_S-Seq and

       A5: (p `1 ) <> (p2 `1 ) and

       A6: (p `2 ) <> (p2 `2 ) and

       A7: h = (f ^ <* |[(p2 `1 ), (p `2 )]|, p*>) and

       A8: ((( LSeg (p2, |[(p2 `1 ), (p `2 )]|)) \/ ( LSeg ( |[(p2 `1 ), (p `2 )]|,p))) /\ ( L~ f)) = {p2};

      set p3 = |[(p2 `1 ), (p `2 )]|, f1 = (f ^ <*p3*>), h1 = (f1 ^ <*p*>);

      reconsider Lf = ( L~ f) as non empty Subset of ( TOP-REAL 2) by A8;

      

       A9: p2 in ( LSeg (p2,p3)) by RLTOPSP1: 68;

      ( L~ f) is_S-P_arc_joining (p1,p2) by A4;

      then Lf is_an_arc_of (p1,p2) by Th2;

      then p2 in ( L~ f) by TOPREAL1: 1;

      then p2 in (( LSeg (p2,p3)) /\ ( L~ f)) by A9, XBOOLE_0:def 4;

      then

       A10: (( LSeg (p2,p3)) /\ ( L~ f)) c= ((( LSeg (p2,p3)) /\ ( L~ f)) \/ (( LSeg (p3,p)) /\ ( L~ f))) & {p2} c= (( LSeg (p2,p3)) /\ ( L~ f)) by XBOOLE_1: 7, ZFMISC_1: 31;

       {p2} = ((( LSeg (p2,p3)) /\ ( L~ f)) \/ (( LSeg (p3,p)) /\ ( L~ f))) by A8, XBOOLE_1: 23;

      then

       A11: (( LSeg (p2,p3)) /\ ( L~ f)) = {p2} by A10;

      

       A12: ( len f1) = (( len f) + ( len <*p3*>)) by FINSEQ_1: 22

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

      then

       A13: (f1 /. ( len f1)) = p3 by FINSEQ_4: 67;

      

       A14: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

       A15: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

      ( len f) >= 2 by A4;

      then

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

      then ( len f) in ( dom f) by A15, FINSEQ_1: 1;

      then

       A17: (f1 /. ( len f)) = p2 by FINSEQ_4: 68;

      

       A18: (( LSeg (p3,p)) /\ ( L~ f1)) c= {p3}

      proof

        set M1 = { ( LSeg (f1,i)) : 1 <= i & (i + 1) <= ( len f1) }, Mf = { ( LSeg (f,j)) : 1 <= j & (j + 1) <= ( len f) };

        assume not thesis;

        then

        consider x be object such that

         A19: x in (( LSeg (p3,p)) /\ ( L~ f1)) and

         A20: not x in {p3};

        x in ( L~ f1) by A19, XBOOLE_0:def 4;

        then

        consider X be set such that

         A21: x in X and

         A22: X in M1 by TARSKI:def 4;

        consider k such that

         A23: X = ( LSeg (f1,k)) and

         A24: 1 <= k and

         A25: (k + 1) <= ( len f1) by A22;

        

         A26: x in ( LSeg (p3,p)) by A19, XBOOLE_0:def 4;

        now

          per cases by A25, XXREAL_0: 1;

            suppose (k + 1) = ( len f1);

            then ( LSeg (f1,k)) = ( LSeg (p2,p3)) by A12, A13, A17, A24, TOPREAL1:def 3;

            then x in (( LSeg (p2,p3)) /\ ( LSeg (p3,p))) by A26, A21, A23, XBOOLE_0:def 4;

            hence contradiction by A20, TOPREAL3: 29;

          end;

            suppose (k + 1) < ( len f1);

            then

             A27: (k + 1) <= ( len f) by A12, NAT_1: 13;

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

            then k <= ( len f) by A27, XXREAL_0: 2;

            then

             A28: k in ( dom f) by A15, A24, FINSEQ_1: 1;

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

            then (k + 1) in ( dom f) by A15, A27, FINSEQ_1: 1;

            then X = ( LSeg (f,k)) by A23, A28, TOPREAL3: 18;

            then X in Mf by A24, A27;

            then

             A29: x in ( L~ f) by A21, TARSKI:def 4;

            x in (( LSeg (p2,p3)) \/ ( LSeg (p3,p))) by A26, XBOOLE_0:def 3;

            then x in {p2} by A8, A29, XBOOLE_0:def 4;

            then x = p2 by TARSKI:def 1;

            hence contradiction by A6, A14, A26, TOPREAL3: 12;

          end;

        end;

        hence contradiction;

      end;

      

       A30: h1 = (f ^ ( <*p3*> ^ <*p*>)) by FINSEQ_1: 32

      .= h by A7, FINSEQ_1:def 9;

      

       A31: (p3 `2 ) = (p `2 ) & (p3 `1 ) = (p2 `1 ) by EUCLID: 52;

      then

       A32: f1 is being_S-Seq by A1, A3, A4, A6, A11, Th19;

      

       A33: ( L~ f1) is_S-P_arc_joining (p1,p3) by A1, A3, A4, A6, A31, A11, Th19;

      then

      reconsider Lf1 = ( L~ f1) as non empty Subset of ( TOP-REAL 2) by Th1, TOPREAL1: 26;

      

       A34: p3 in ( LSeg (p3,p)) by RLTOPSP1: 68;

      

       A35: (f1 /. ( len f1)) = p3 by A12, FINSEQ_4: 67;

      ( L~ f1) c= (( L~ f) \/ ( Ball (u,r))) by A1, A3, A4, A6, A31, A11, Th19;

      then (( L~ f1) \/ ( Ball (u,r))) c= ((( L~ f) \/ ( Ball (u,r))) \/ ( Ball (u,r))) by XBOOLE_1: 9;

      then

       A36: (( L~ f1) \/ ( Ball (u,r))) c= (( L~ f) \/ (( Ball (u,r)) \/ ( Ball (u,r)))) by XBOOLE_1: 4;

      

       A37: (p `1 ) = (p3 `1 ) & (p `2 ) <> (p3 `2 ) or (p `1 ) <> (p3 `1 ) & (p `2 ) = (p3 `2 ) by A5, EUCLID: 52;

      Lf1 is_an_arc_of (p1,p3) by A33, Th2;

      then p3 in ( L~ f1) by TOPREAL1: 1;

      then p3 in (( LSeg (p3,p)) /\ ( L~ f1)) by A34, XBOOLE_0:def 4;

      then {p3} c= (( LSeg (p3,p)) /\ ( L~ f1)) by ZFMISC_1: 31;

      then

       A38: (( LSeg (p3,p)) /\ ( L~ f1)) = {p3} by A18;

      1 in ( dom f) by A15, A16, FINSEQ_1: 1;

      then (f1 /. 1) = p1 by FINSEQ_4: 68;

      hence ( L~ h) is_S-P_arc_joining (p1,p) by A2, A3, A37, A32, A35, A38, A30, Th19;

      ( L~ h1) c= (( L~ f1) \/ ( Ball (u,r))) by A2, A3, A37, A32, A35, A38, Th19;

      hence thesis by A30, A36;

    end;

    theorem :: TOPREAL4:22

    

     Th22: not (f /. 1) in ( Ball (u,r)) & (f /. ( len f)) in ( Ball (u,r)) & p in ( Ball (u,r)) & f is being_S-Seq & not p in ( L~ f) implies ex h st ( L~ h) is_S-P_arc_joining ((f /. 1),p) & ( L~ h) c= (( L~ f) \/ ( Ball (u,r)))

    proof

      set p1 = (f /. 1);

      set Mf = { ( LSeg (f,k)) : 1 <= k & (k + 1) <= ( len f) };

      assume that

       A1: not p1 in ( Ball (u,r)) and

       A2: (f /. ( len f)) in ( Ball (u,r)) and

       A3: p in ( Ball (u,r)) and

       A4: f is being_S-Seq and

       A5: not p in ( L~ f);

      

       A6: f is special by A4;

      defpred X[ Nat] means 1 <= $1 & $1 <= (( len f) - 1) & ( LSeg (f,$1)) meets ( Ball (u,r));

      

       A7: ( len f) >= 2 by A4;

      then

      reconsider n = (( len f) - 1) as Element of NAT by INT_1: 5, XXREAL_0: 2;

      2 = (1 + 1);

      then

       A8: 1 <= (( len f) - 1) by A7, XREAL_1: 19;

      (n + 1) = ( len f);

      then (f /. ( len f)) in ( LSeg (f,n)) by A8, TOPREAL1: 21;

      then ( LSeg (f,n)) meets ( Ball (u,r)) by A2, XBOOLE_0: 3;

      then

       A9: ex n be Nat st X[n] by A8;

      consider m be Nat such that

       A10: X[m] and

       A11: for i be Nat st X[i] holds m <= i from NAT_1:sch 5( A9);

      reconsider m as Element of NAT by ORDINAL1:def 12;

      consider q1, q2 such that

       A12: (f /. m) = q1 and

       A13: (f /. (m + 1)) = q2;

      

       A14: (( LSeg (f,m)) /\ ( Ball (u,r))) <> {} by A10, XBOOLE_0:def 7;

      

       A15: (m + 1) <= ( len f) by A10, XREAL_1: 19;

      then

       A16: ( LSeg (f,m)) = ( LSeg (q1,q2)) by A10, A12, A13, TOPREAL1:def 3;

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

      then

       A17: m <= ( len f) by A15, XXREAL_0: 2;

      

       A18: ( Seg ( len f)) = ( dom f) by FINSEQ_1:def 3;

       A19:

      now

        set x = the Element of (( Ball (u,r)) /\ ( L~ (f | m)));

        set M = { ( LSeg ((f | m),i)) : 1 <= i & (i + 1) <= ( len (f | m)) };

        

         A20: ( Seg ( len (f | m))) = ( dom (f | m)) by FINSEQ_1:def 3;

        assume

         A21: (( Ball (u,r)) /\ ( L~ (f | m))) <> {} ;

        then

         A22: x in ( Ball (u,r)) by XBOOLE_0:def 4;

        x in ( L~ (f | m)) by A21, XBOOLE_0:def 4;

        then

        consider X be set such that

         A23: x in X and

         A24: X in M by TARSKI:def 4;

        consider k such that

         A25: X = ( LSeg ((f | m),k)) and

         A26: 1 <= k and

         A27: (k + 1) <= ( len (f | m)) by A24;

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

        then k <= ( len (f | m)) by A27, XXREAL_0: 2;

        then

         A28: k in ( Seg ( len (f | m))) by A26, FINSEQ_1: 1;

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

        then (k + 1) in ( Seg ( len (f | m))) by A27, FINSEQ_1: 1;

        then x in ( LSeg (f,k)) by A23, A25, A28, A20, TOPREAL3: 17;

        then

         A29: ( LSeg (f,k)) meets ( Ball (u,r)) by A22, XBOOLE_0: 3;

        ( Seg m) c= ( Seg ( len f)) by A17, FINSEQ_1: 5;

        

        then

         A30: ( Seg m) = (( dom f) /\ ( Seg m)) by A18, XBOOLE_1: 28

        .= ( dom (f | ( Seg m))) by RELAT_1: 61

        .= ( Seg ( len (f | m))) by A20, FINSEQ_1:def 15;

        

         A31: ((k + 1) - 1) <= (( len (f | m)) - 1) by A27, XREAL_1: 9;

        then

         A32: k <= (m - 1) by A30, FINSEQ_1: 6;

        m = ( len (f | m)) by A30, FINSEQ_1: 6;

        then (( len (f | m)) - 1) <= (( len f) - 1) by A17, XREAL_1: 9;

        then k <= (( len f) - 1) by A31, XXREAL_0: 2;

        then m <= k by A11, A26, A29;

        then m <= (m - 1) by A32, XXREAL_0: 2;

        then 0 <= ((m + ( - 1)) - m) by XREAL_1: 48;

        hence contradiction;

      end;

      for i st 1 <= i <= (( len f) - 1) & (( LSeg (f,i)) /\ ( Ball (u,r))) <> {} holds m <= i by A11, XBOOLE_0:def 7;

      then

       A33: not q1 in ( Ball (u,r)) by A1, A10, A12, TOPREAL3: 26;

      set A = (( LSeg (f,m)) /\ ( Ball (u,r)));

      

       A34: q1 = |[(q1 `1 ), (q1 `2 )]| & q2 = |[(q2 `1 ), (q2 `2 )]| by EUCLID: 53;

      (m + 1) <= (n + 1) by A10, XREAL_1: 6;

      then ( LSeg (f,m)) in Mf by A10;

      then

       A35: ( LSeg (f,m)) c= ( union Mf) by ZFMISC_1: 74;

      now

        per cases ;

          suppose ex q st q in A & ((p `1 ) = (q `1 ) or (p `2 ) = (q `2 ));

          then

          consider q such that

           A36: q in A and

           A37: (p `1 ) = (q `1 ) or (p `2 ) = (q `2 );

          

           A38: q in ( Ball (u,r)) by A36, XBOOLE_0:def 4;

          

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

          

           A40: q in ( LSeg (f,m)) by A36, XBOOLE_0:def 4;

          then

          consider h such that

           A41: h is being_S-Seq and

           A42: (h /. 1) = p1 and

           A43: (h /. ( len h)) = q and

           A44: ( L~ h) is_S-P_arc_joining (p1,q) and

           A45: ( L~ h) c= ( L~ f) and

           A46: ( L~ h) = (( L~ (f | m)) \/ ( LSeg (q1,q))) by A1, A4, A12, A38, Th17;

          take g = (h ^ <*p*>);

          

           A47: (( L~ h) \/ ( Ball (u,r))) c= (( L~ f) \/ ( Ball (u,r))) by A45, XBOOLE_1: 9;

          

           A48: q in ( L~ f) by A35, A40;

           A49:

          now

            per cases by A37;

              suppose (p `1 ) = (q `1 );

              hence (p `1 ) = (q `1 ) & (p `2 ) <> (q `2 ) or (p `1 ) <> (q `1 ) & (p `2 ) = (q `2 ) by A5, A48, TOPREAL3: 6;

            end;

              suppose (p `2 ) = (q `2 );

              hence (p `1 ) = (q `1 ) & (p `2 ) <> (q `2 ) or (p `1 ) <> (q `1 ) & (p `2 ) = (q `2 ) by A5, A48, TOPREAL3: 6;

            end;

          end;

          

           A50: (( LSeg (q,p)) /\ ( L~ h)) c= {q}

          proof

             A51:

            now

              per cases by A6, A10, A15, A12, A13;

                suppose (q1 `1 ) = (q2 `1 );

                hence (q1 `1 ) = (q `1 ) or (q1 `2 ) = (q `2 ) by A34, A16, A40, TOPREAL3: 11;

              end;

                suppose (q1 `2 ) = (q2 `2 );

                hence (q1 `1 ) = (q `1 ) or (q1 `2 ) = (q `2 ) by A34, A16, A40, TOPREAL3: 12;

              end;

            end;

            ( LSeg (q,p)) = (( LSeg (q,p)) /\ ( Ball (u,r))) by A3, A38, TOPREAL3: 21, XBOOLE_1: 28;

            

            then

             A52: (( LSeg (q,p)) /\ (( L~ (f | m)) \/ ( LSeg (q1,q)))) = (((( LSeg (q,p)) /\ ( Ball (u,r))) /\ ( L~ (f | m))) \/ (( LSeg (q,p)) /\ ( LSeg (q1,q)))) by XBOOLE_1: 23

            .= ((( LSeg (q,p)) /\ (( Ball (u,r)) /\ ( L~ (f | m)))) \/ (( LSeg (q,p)) /\ ( LSeg (q1,q)))) by XBOOLE_1: 16

            .= (( LSeg (q1,q)) /\ ( LSeg (q,p))) by A19;

             A53:

            now

              q1 in ( LSeg (q1,q2)) by RLTOPSP1: 68;

              then

               A54: ( LSeg (q1,q)) c= ( LSeg (f,m)) by A16, A40, TOPREAL1: 6;

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

              hence contradiction by A5, A35, A54;

            end;

            let x be object;

            assume x in (( LSeg (q,p)) /\ ( L~ h));

            hence thesis by A3, A33, A38, A49, A46, A52, A53, A51, TOPREAL3: 42;

          end;

          q in ( L~ h) by A44, Th3;

          then q in (( LSeg (q,p)) /\ ( L~ h)) by A39, XBOOLE_0:def 4;

          then {q} c= (( LSeg (q,p)) /\ ( L~ h)) by ZFMISC_1: 31;

          then

           A55: (( LSeg (q,p)) /\ ( L~ h)) = {q} by A50;

          then ( L~ g) c= (( L~ h) \/ ( Ball (u,r))) by A3, A38, A49, A41, A43, Th19;

          hence ( L~ g) is_S-P_arc_joining (p1,p) & ( L~ g) c= (( L~ f) \/ ( Ball (u,r))) by A3, A38, A49, A41, A42, A43, A55, A47, Th19;

        end;

          suppose

           A56: for q st q in A holds (p `1 ) <> (q `1 ) & (p `2 ) <> (q `2 );

          set x = the Element of A;

          

           A57: x in ( LSeg (f,m)) by A14, XBOOLE_0:def 4;

          then

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

          

           A58: (q `1 ) <> (p `1 ) & (q `2 ) <> (p `2 ) by A14, A56;

          q <> p1 by A1, A14, XBOOLE_0:def 4;

          then

          consider h such that

           A59: h is being_S-Seq and

           A60: (h /. 1) = p1 and

           A61: (h /. ( len h)) = q and

           A62: ( L~ h) is_S-P_arc_joining (p1,q) and

           A63: ( L~ h) c= ( L~ f) and

           A64: ( L~ h) = (( L~ (f | m)) \/ ( LSeg (q1,q))) by A4, A12, A57, Th17;

          

           A65: q in ( Ball (u,r)) by A14, XBOOLE_0:def 4;

          

           A66: q = |[(q `1 ), (q `2 )]| & p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

          now

            per cases by A3, A65, A66, TOPREAL3: 25;

              suppose

               A67: |[(q `1 ), (p `2 )]| in ( Ball (u,r));

              set v = |[(q `1 ), (p `2 )]|;

              

               A68: ((( LSeg (q,v)) \/ ( LSeg (v,p))) /\ ( L~ h)) c= {q}

              proof

                let x be object;

                set L = (( LSeg (q,v)) \/ ( LSeg (v,p)));

                assume

                 A69: x in (L /\ ( L~ h));

                ( LSeg (q,v)) c= ( Ball (u,r)) & ( LSeg (v,p)) c= ( Ball (u,r)) by A3, A65, A67, TOPREAL3: 21;

                then L = (L /\ ( Ball (u,r))) by XBOOLE_1: 8, XBOOLE_1: 28;

                

                then

                 A70: (L /\ (( L~ (f | m)) \/ ( LSeg (q1,q)))) = (((L /\ ( Ball (u,r))) /\ ( L~ (f | m))) \/ (L /\ ( LSeg (q1,q)))) by XBOOLE_1: 23

                .= ((L /\ (( Ball (u,r)) /\ ( L~ (f | m)))) \/ (L /\ ( LSeg (q1,q)))) by XBOOLE_1: 16

                .= ( {} \/ (L /\ ( LSeg (q1,q)))) by A19;

                 A71:

                now

                  per cases by A6, A10, A15, A12, A13;

                    suppose (q1 `1 ) = (q2 `1 );

                    hence (q1 `1 ) = (q `1 ) or (q1 `2 ) = (q `2 ) by A34, A16, A57, TOPREAL3: 11;

                  end;

                    suppose (q1 `2 ) = (q2 `2 );

                    hence (q1 `1 ) = (q `1 ) or (q1 `2 ) = (q `2 ) by A34, A16, A57, TOPREAL3: 12;

                  end;

                end;

                now

                  per cases by A71;

                    suppose

                     A72: (q1 `1 ) = (q `1 );

                    now

                      q1 in ( LSeg (q1,q2)) by RLTOPSP1: 68;

                      then

                       A73: ( LSeg (q1,q)) c= ( LSeg (f,m)) by A16, A57, TOPREAL1: 6;

                      

                       A74: (v `2 ) = (p `2 ) by EUCLID: 52;

                      assume v in ( LSeg (q1,q));

                      then v in (( LSeg (f,m)) /\ ( Ball (u,r))) by A67, A73, XBOOLE_0:def 4;

                      hence contradiction by A56, A74;

                    end;

                    hence thesis by A33, A65, A58, A64, A67, A70, A69, A72, TOPREAL3: 43;

                  end;

                    suppose (q1 `2 ) = (q `2 );

                    hence thesis by A14, A56, A64, A70, A69, TOPREAL3: 27;

                  end;

                end;

                hence thesis;

              end;

              take g = (h ^ <* |[(q `1 ), (p `2 )]|, p*>);

              q in ( LSeg (q,v)) by RLTOPSP1: 68;

              then

               A75: q in (( LSeg (q,v)) \/ ( LSeg (v,p))) by XBOOLE_0:def 3;

              

               A76: (( L~ h) \/ ( Ball (u,r))) c= (( L~ f) \/ ( Ball (u,r))) by A63, XBOOLE_1: 9;

              q in ( L~ h) by A62, Th3;

              then q in ((( LSeg (q,v)) \/ ( LSeg (v,p))) /\ ( L~ h)) by A75, XBOOLE_0:def 4;

              then {q} c= ((( LSeg (q,v)) \/ ( LSeg (v,p))) /\ ( L~ h)) by ZFMISC_1: 31;

              then

               A77: ((( LSeg (q, |[(q `1 ), (p `2 )]|)) \/ ( LSeg ( |[(q `1 ), (p `2 )]|,p))) /\ ( L~ h)) = {q} by A68;

              then ( L~ g) c= (( L~ h) \/ ( Ball (u,r))) by A3, A65, A58, A59, A61, A67, Th21;

              hence ( L~ g) is_S-P_arc_joining (p1,p) & ( L~ g) c= (( L~ f) \/ ( Ball (u,r))) by A3, A65, A58, A59, A60, A61, A67, A77, A76, Th21;

            end;

              suppose

               A78: |[(p `1 ), (q `2 )]| in ( Ball (u,r));

              set v = |[(p `1 ), (q `2 )]|;

              

               A79: ((( LSeg (q,v)) \/ ( LSeg (v,p))) /\ ( L~ h)) c= {q}

              proof

                let x be object;

                set L = (( LSeg (q,v)) \/ ( LSeg (v,p)));

                assume

                 A80: x in (L /\ ( L~ h));

                ( LSeg (q,v)) c= ( Ball (u,r)) & ( LSeg (v,p)) c= ( Ball (u,r)) by A3, A65, A78, TOPREAL3: 21;

                then L = (L /\ ( Ball (u,r))) by XBOOLE_1: 8, XBOOLE_1: 28;

                

                then

                 A81: (L /\ (( L~ (f | m)) \/ ( LSeg (q1,q)))) = (((L /\ ( Ball (u,r))) /\ ( L~ (f | m))) \/ (L /\ ( LSeg (q1,q)))) by XBOOLE_1: 23

                .= ((L /\ (( Ball (u,r)) /\ ( L~ (f | m)))) \/ (L /\ ( LSeg (q1,q)))) by XBOOLE_1: 16

                .= ( {} \/ (L /\ ( LSeg (q1,q)))) by A19;

                 A82:

                now

                  per cases by A6, A10, A15, A12, A13;

                    suppose (q1 `1 ) = (q2 `1 );

                    hence (q1 `1 ) = (q `1 ) or (q1 `2 ) = (q `2 ) by A34, A16, A57, TOPREAL3: 11;

                  end;

                    suppose (q1 `2 ) = (q2 `2 );

                    hence (q1 `1 ) = (q `1 ) or (q1 `2 ) = (q `2 ) by A34, A16, A57, TOPREAL3: 12;

                  end;

                end;

                now

                  per cases by A82;

                    suppose (q1 `1 ) = (q `1 );

                    hence thesis by A14, A56, A64, A81, A80, TOPREAL3: 28;

                  end;

                    suppose

                     A83: (q1 `2 ) = (q `2 );

                    now

                      q1 in ( LSeg (q1,q2)) by RLTOPSP1: 68;

                      then

                       A84: ( LSeg (q1,q)) c= ( LSeg (f,m)) by A16, A57, TOPREAL1: 6;

                      

                       A85: (v `1 ) = (p `1 ) by EUCLID: 52;

                      assume v in ( LSeg (q1,q));

                      then v in (( LSeg (f,m)) /\ ( Ball (u,r))) by A78, A84, XBOOLE_0:def 4;

                      hence contradiction by A56, A85;

                    end;

                    hence thesis by A33, A65, A58, A64, A78, A81, A80, A83, TOPREAL3: 44;

                  end;

                end;

                hence thesis;

              end;

              take g = (h ^ <* |[(p `1 ), (q `2 )]|, p*>);

              q in ( LSeg (q,v)) by RLTOPSP1: 68;

              then

               A86: q in (( LSeg (q,v)) \/ ( LSeg (v,p))) by XBOOLE_0:def 3;

              

               A87: (( L~ h) \/ ( Ball (u,r))) c= (( L~ f) \/ ( Ball (u,r))) by A63, XBOOLE_1: 9;

              q in ( L~ h) by A62, Th3;

              then q in ((( LSeg (q,v)) \/ ( LSeg (v,p))) /\ ( L~ h)) by A86, XBOOLE_0:def 4;

              then {q} c= ((( LSeg (q,v)) \/ ( LSeg (v,p))) /\ ( L~ h)) by ZFMISC_1: 31;

              then

               A88: ((( LSeg (q, |[(p `1 ), (q `2 )]|)) \/ ( LSeg ( |[(p `1 ), (q `2 )]|,p))) /\ ( L~ h)) = {q} by A79;

              then ( L~ g) c= (( L~ h) \/ ( Ball (u,r))) by A3, A65, A58, A59, A61, A78, Th20;

              hence ( L~ g) is_S-P_arc_joining (p1,p) & ( L~ g) c= (( L~ f) \/ ( Ball (u,r))) by A3, A65, A58, A59, A60, A61, A78, A88, A87, Th20;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL4:23

    

     Th23: for R, p, p1, p2, P, r, u st p <> p1 & P is_S-P_arc_joining (p1,p2) & P c= R & p in ( Ball (u,r)) & p2 in ( Ball (u,r)) & ( Ball (u,r)) c= R holds ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p1,p) & P1 c= R

    proof

      let R, p, p1, p2, P, r, u;

      assume that

       A1: p <> p1 and

       A2: P is_S-P_arc_joining (p1,p2) and

       A3: P c= R and

       A4: p in ( Ball (u,r)) and

       A5: p2 in ( Ball (u,r)) and

       A6: ( Ball (u,r)) c= R;

      consider f such that

       A7: f is being_S-Seq and

       A8: P = ( L~ f) and

       A9: p1 = (f /. 1) and

       A10: p2 = (f /. ( len f)) by A2;

      now

        per cases ;

          suppose p1 in ( Ball (u,r));

          then

          consider P1 such that

           A11: P1 is_S-P_arc_joining (p1,p) & P1 c= ( Ball (u,r)) by A1, A4, Th10;

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

          take P1;

          thus P1 is_S-P_arc_joining (p1,p) & P1 c= R by A6, A11;

        end;

          suppose

           A12: not p1 in ( Ball (u,r));

          now

            per cases ;

              suppose p in P;

              then

              consider h such that h is being_S-Seq and (h /. 1) = p1 and (h /. ( len h)) = p and

               A13: ( L~ h) is_S-P_arc_joining (p1,p) & ( L~ h) c= ( L~ f) by A1, A7, A8, A9, Th18;

              reconsider P1 = ( L~ h) as Subset of ( TOP-REAL 2);

              take P1;

              thus P1 is_S-P_arc_joining (p1,p) & P1 c= R by A3, A8, A13;

            end;

              suppose not p in P;

              then

              consider h such that

               A14: ( L~ h) is_S-P_arc_joining (p1,p) and

               A15: ( L~ h) c= (( L~ f) \/ ( Ball (u,r))) by A4, A5, A7, A8, A9, A10, A12, Th22;

              reconsider P1 = ( L~ h) as Subset of ( TOP-REAL 2);

              take P1;

              thus P1 is_S-P_arc_joining (p1,p) by A14;

              (( L~ f) \/ ( Ball (u,r))) c= R by A3, A6, A8, XBOOLE_1: 8;

              hence P1 c= R by A15;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

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

    reserve P,R for Subset of ( TOP-REAL 2);

    theorem :: TOPREAL4:24

    

     Th24: for p st R is being_Region & P = { q : q <> p & q in R & not ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R } holds P is open

    proof

      let p;

      assume that

       A1: R is being_Region and

       A2: P = { q : q <> p & q in R & not ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R };

      reconsider RR = R, PP = P as Subset of the TopStruct of ( TOP-REAL 2);

      R is open by A1;

      then

       A3: RR is open by PRE_TOPC: 30;

      now

        let u;

        reconsider p2 = u as Point of ( TOP-REAL 2) by TOPREAL3: 8;

        assume

         A4: u in P;

        then ex q1 st q1 = u & q1 <> p & q1 in R & not ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q1) & P1 c= R by A2;

        then

        consider r be Real such that

         A5: r > 0 and

         A6: ( Ball (u,r)) c= RR by A3, Lm1, TOPMETR: 15;

        take r;

        thus r > 0 by A5;

        reconsider r9 = r as Real;

        

         A7: p2 in ( Ball (u,r9)) by A5, TBSP_1: 11;

        thus ( Ball (u,r)) c= P

        proof

          assume not thesis;

          then

          consider x be object such that

           A8: x in ( Ball (u,r)) and

           A9: not x in P;

          x in R by A6, A8;

          then

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

          now

            per cases by A2, A6, A8, A9;

              suppose

               A10: q = p;

               A11:

              now

                assume

                 A12: q = p2;

                ex p3 st p3 = p2 & p3 <> p & p3 in R & not ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,p3) & P1 c= R by A2, A4;

                hence contradiction by A10, A12;

              end;

              u in ( Ball (u,r9)) by A5, TBSP_1: 11;

              then

               A13: ex P2 be Subset of ( TOP-REAL 2) st P2 is_S-P_arc_joining (q,p2) & P2 c= ( Ball (u,r9)) by A8, A11, Th10;

               not p2 in P

              proof

                assume p2 in P;

                then ex q4 st q4 = p2 & q4 <> p & q4 in R & not ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q4) & P1 c= R by A2;

                hence contradiction by A6, A10, A13, XBOOLE_1: 1;

              end;

              hence contradiction by A4;

            end;

              suppose

               A14: ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R;

               not p2 in P

              proof

                assume p2 in P;

                then ex q4 st q4 = p2 & q4 <> p & q4 in R & not ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q4) & P1 c= R by A2;

                hence contradiction by A6, A7, A8, A14, Th23;

              end;

              hence contradiction by A4;

            end;

          end;

          hence contradiction;

        end;

      end;

      then PP is open by Lm1, TOPMETR: 15;

      hence thesis by PRE_TOPC: 30;

    end;

    theorem :: TOPREAL4:25

    

     Th25: R is being_Region & p in R & P = { q : q = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R } implies P is open

    proof

      assume that

       A1: R is being_Region and

       A2: p in R and

       A3: P = { q : q = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R };

      reconsider RR = R, PP = P as Subset of the TopStruct of ( TOP-REAL 2);

      R is open by A1;

      then

       A4: RR is open by PRE_TOPC: 30;

      now

        let u;

        reconsider p2 = u as Point of ( TOP-REAL 2) by TOPREAL3: 8;

        assume u in P;

        then

        consider q1 such that

         A5: q1 = u and

         A6: q1 = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q1) & P1 c= R by A3;

        now

          per cases by A6;

            suppose q1 = p;

            hence p2 in R by A2, A5;

          end;

            suppose ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q1) & P1 c= R;

            then

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

             A7: P2 is_S-P_arc_joining (p,q1) and

             A8: P2 c= R;

            p2 in P2 by A5, A7, Th3;

            hence p2 in R by A8;

          end;

        end;

        then

        consider r be Real such that

         A9: r > 0 and

         A10: ( Ball (u,r)) c= RR by A4, Lm1, TOPMETR: 15;

        take r;

        thus r > 0 by A9;

        reconsider r9 = r as Real;

        

         A11: p2 in ( Ball (u,r9)) by A9, TBSP_1: 11;

        thus ( Ball (u,r)) c= P

        proof

          let x be object;

          assume

           A12: x in ( Ball (u,r));

          then

          reconsider q = x as Point of ( TOP-REAL 2) by A10, TARSKI:def 3;

          now

            per cases ;

              suppose q = p;

              hence thesis by A3;

            end;

              suppose

               A13: q <> p;

               A14:

              now

                assume q1 = p;

                then p in ( Ball (u,r9)) by A5, A9, TBSP_1: 11;

                then

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

                 A15: P2 is_S-P_arc_joining (p,q) and

                 A16: P2 c= ( Ball (u,r9)) by A12, A13, Th10;

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

                P2 c= R by A10, A16;

                hence thesis by A3, A15;

              end;

              now

                assume q1 <> p;

                then ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R by A5, A6, A10, A11, A12, A13, Th23;

                hence thesis by A3;

              end;

              hence thesis by A14;

            end;

          end;

          hence thesis;

        end;

      end;

      then PP is open by Lm1, TOPMETR: 15;

      hence thesis by PRE_TOPC: 30;

    end;

    theorem :: TOPREAL4:26

    

     Th26: p in R & P = { q : q = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R } implies P c= R

    proof

      assume that

       A1: p in R and

       A2: P = { q : q = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R };

      let x be object;

      assume x in P;

      then

      consider q such that

       A3: q = x and

       A4: q = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R by A2;

      now

        per cases by A4;

          suppose q = p;

          hence thesis by A1, A3;

        end;

          suppose ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R;

          then

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

           A5: P1 is_S-P_arc_joining (p,q) and

           A6: P1 c= R;

          q in P1 by A5, Th3;

          hence thesis by A3, A6;

        end;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL4:27

    

     Th27: R is being_Region & p in R & P = { q : q = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R } implies R c= P

    proof

      assume that

       A1: R is being_Region and

       A2: p in R and

       A3: P = { q : q = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R };

      

       A4: p in P by A3;

      set P2 = (R \ P);

      reconsider P22 = P2 as Subset of ( TOP-REAL 2);

      

       A5: ( [#] (( TOP-REAL 2) | R)) = R by PRE_TOPC:def 5;

      then

      reconsider P11 = P, P12 = P22 as Subset of (( TOP-REAL 2) | R) by A2, A3, Th26, XBOOLE_1: 36;

      (P \/ (R \ P)) = (P \/ R) by XBOOLE_1: 39;

      then

       A6: ( [#] (( TOP-REAL 2) | R)) = (P11 \/ P12) by A5, XBOOLE_1: 12;

      now

        let x be object;

         A7:

        now

          assume

           A8: x in P2;

          then

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

           not x in P by A8, XBOOLE_0:def 5;

          then

           A9: q2 <> p & not ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q2) & P1 c= R by A3;

          q2 in R by A8, XBOOLE_0:def 5;

          hence x in { q : q <> p & q in R & not ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R } by A9;

        end;

        now

          assume x in { q : q <> p & q in R & not ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R };

          then

           A10: ex q3 st q3 = x & q3 <> p & q3 in R & not ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q3) & P1 c= R;

          then not ex q st q = x & (q = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R);

          then not x in P by A3;

          hence x in P2 by A10, XBOOLE_0:def 5;

        end;

        hence x in P2 iff x in { q : q <> p & q in R & not ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R } by A7;

      end;

      then P2 = { q : q <> p & q in R & not ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R } by TARSKI: 2;

      then P22 is open by A1, Th24;

      then

       A11: P22 in the topology of ( TOP-REAL 2) by PRE_TOPC:def 2;

      reconsider R9 = R as non empty Subset of ( TOP-REAL 2) by A2;

      R is connected by A1;

      then

       A12: (( TOP-REAL 2) | R9) is connected by CONNSP_1:def 3;

      P is open by A1, A2, A3, Th25;

      then

       A13: P in the topology of ( TOP-REAL 2) by PRE_TOPC:def 2;

      P11 = (P /\ ( [#] (( TOP-REAL 2) | R))) by XBOOLE_1: 28;

      then P11 in the topology of (( TOP-REAL 2) | R) by A13, PRE_TOPC:def 4;

      then

       A14: P11 is open by PRE_TOPC:def 2;

      P12 = (P22 /\ ( [#] (( TOP-REAL 2) | R))) by XBOOLE_1: 28;

      then P12 in the topology of (( TOP-REAL 2) | R) by A11, PRE_TOPC:def 4;

      then

       A15: P12 is open by PRE_TOPC:def 2;

      

       A16: P11 misses P12 by XBOOLE_1: 79;

      then (P11 /\ P12) = ( {} (( TOP-REAL 2) | R));

      then P2 = {} by A4, A12, A16, A6, A14, A15, CONNSP_1: 11;

      hence thesis by XBOOLE_1: 37;

    end;

    theorem :: TOPREAL4:28

    R is being_Region & p in R & P = { q : q = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q) & P1 c= R } implies R = P by Th27, Th26;

    theorem :: TOPREAL4:29

    R is being_Region & p in R & q in R & p <> q implies ex P st P is_S-P_arc_joining (p,q) & P c= R

    proof

      set RR = { q2 : q2 = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q2) & P1 c= R };

      RR c= the carrier of ( TOP-REAL 2)

      proof

        let x be object;

        assume x in RR;

        then ex q2 st q2 = x & (q2 = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q2) & P1 c= R);

        hence thesis;

      end;

      then

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

      assume that

       A1: R is being_Region & p in R and

       A2: q in R and

       A3: p <> q;

      R c= RR by A1, Th27;

      then q in RR by A2;

      then ex q1 st q1 = q & (q1 = p or ex P1 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p,q1) & P1 c= R);

      hence thesis by A3;

    end;