topreal1.miz



    begin

    reserve r,lambda for Real,

i,j,n for Nat;

    scheme :: TOPREAL1:sch1

    FraenkelAlt { A() -> non empty set , P[ set], Q[ set] } :

{ v where v be Element of A() : P[v] or Q[v] } = ({ v1 where v1 be Element of A() : P[v1] } \/ { v2 where v2 be Element of A() : Q[v2] });

      set X = { v where v be Element of A() : P[v] or Q[v] }, Y = { v1 where v1 be Element of A() : P[v1] }, Z = { v2 where v2 be Element of A() : Q[v2] };

      now

        let x be object;

        thus for x be object holds x in X implies x in (Y \/ Z)

        proof

          let x be object;

          assume x in X;

          then

          consider v be Element of A() such that

           A1: x = v and

           A2: P[v] or Q[v];

          per cases by A2;

            suppose P[v];

            then x in Y by A1;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose Q[v];

            then x in Z by A1;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        assume

         A3: x in (Y \/ Z);

        per cases by A3, XBOOLE_0:def 3;

          suppose x in Y;

          then ex v be Element of A() st x = v & P[v];

          hence x in X;

        end;

          suppose x in Z;

          then ex v be Element of A() st x = v & Q[v];

          hence x in X;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    reserve p,p1,p2,q1,q2 for Point of ( TOP-REAL 2),

P,P1 for Subset of ( TOP-REAL 2);

    reserve T for TopSpace;

    definition

      let T;

      let p1,p2 be Point of T, P be Subset of T;

      :: TOPREAL1:def1

      pred P is_an_arc_of p1,p2 means ex f be Function of I[01] , (T | P) st f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = p2;

    end

    theorem :: TOPREAL1:1

    

     Th1: for P be Subset of T, p1,p2 be Point of T st P is_an_arc_of (p1,p2) holds p1 in P & p2 in P

    proof

      let P be Subset of T, p1,p2 be Point of T;

      assume P is_an_arc_of (p1,p2);

      then

      consider f be Function of I[01] , (T | P) such that

       A1: f is being_homeomorphism and

       A2: (f . 0 ) = p1 and

       A3: (f . 1) = p2;

      

       A4: ( dom f) = ( [#] I[01] ) by A1, TOPS_2:def 5

      .= the carrier of I[01] ;

      1 in [. 0 , 1.] by XXREAL_1: 1;

      then

       A5: p2 in ( rng f) by A3, A4, BORSUK_1: 40, FUNCT_1:def 3;

      

       A6: ( rng f) = ( [#] (T | P)) by A1, TOPS_2:def 5;

       0 in [. 0 , 1.] by XXREAL_1: 1;

      then p1 in ( rng f) by A2, A4, BORSUK_1: 40, FUNCT_1:def 3;

      hence thesis by A5, A6, PRE_TOPC:def 5;

    end;

    theorem :: TOPREAL1:2

    

     Th2: for T be T_2 TopSpace holds for P,Q be Subset of T, p1,p2,q1 be Point of T st P is_an_arc_of (p1,p2) & Q is_an_arc_of (p2,q1) & (P /\ Q) = {p2} holds (P \/ Q) is_an_arc_of (p1,q1) by TOPMETR2: 3;

    definition

      :: TOPREAL1:def2

      func R^2-unit_square -> Subset of ( TOP-REAL 2) equals ((( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) \/ ( LSeg ( |[ 0 , 1]|, |[1, 1]|))) \/ (( LSeg ( |[1, 1]|, |[1, 0 ]|)) \/ ( LSeg ( |[1, 0 ]|, |[ 0 , 0 ]|))));

      coherence ;

    end

    

     Lm1: for p,p1,p2 be Point of ( TOP-REAL n) st p in ( LSeg (p1,p2)) holds ( LSeg (p1,p)) c= ( LSeg (p1,p2))

    proof

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

      assume p in ( LSeg (p1,p2));

      then

      consider r such that

       A1: p = (((1 - r) * p1) + (r * p2)) and

       A2: 0 <= r and

       A3: r <= 1;

      let q be object;

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

      then

      consider b be Real such that

       A4: q = (((1 - b) * p1) + (b * p)) and

       A5: 0 <= b and

       A6: b <= 1;

      

       A7: q = (((1 - b) * p1) + ((b * ((1 - r) * p1)) + (b * (r * p2)))) by A1, A4, RLVECT_1:def 5

      .= ((((1 - b) * p1) + (b * ((1 - r) * p1))) + (b * (r * p2))) by RLVECT_1:def 3

      .= ((((1 - b) * p1) + ((b * (1 - r)) * p1)) + (b * (r * p2))) by RLVECT_1:def 7

      .= ((((1 - b) + (b * (1 - r))) * p1) + (b * (r * p2))) by RLVECT_1:def 6

      .= (((1 - (b * r)) * p1) + ((b * r) * p2)) by RLVECT_1:def 7;

      (b * r) <= 1 by A2, A3, A6, XREAL_1: 160;

      hence thesis by A2, A5, A7;

    end;

    theorem :: TOPREAL1:3

    (p1 `1 ) <= (p2 `1 ) & p in ( LSeg (p1,p2)) implies (p1 `1 ) <= (p `1 ) & (p `1 ) <= (p2 `1 )

    proof

      assume that

       A1: (p1 `1 ) <= (p2 `1 ) and

       A2: p in ( LSeg (p1,p2));

      consider lambda such that

       A3: p = (((1 - lambda) * p1) + (lambda * p2)) and

       A4: 0 <= lambda and

       A5: lambda <= 1 by A2;

      

       A6: (((1 - lambda) * p1) `1 ) = ( |[((1 - lambda) * (p1 `1 )), ((1 - lambda) * (p1 `2 ))]| `1 ) by EUCLID: 57

      .= ((1 - lambda) * (p1 `1 )) by EUCLID: 52;

      

       A7: ((lambda * p2) `1 ) = ( |[(lambda * (p2 `1 )), (lambda * (p2 `2 ))]| `1 ) by EUCLID: 57

      .= (lambda * (p2 `1 )) by EUCLID: 52;

      

       A8: (p `1 ) = ( |[((((1 - lambda) * p1) `1 ) + ((lambda * p2) `1 )), ((((1 - lambda) * p1) `2 ) + ((lambda * p2) `2 ))]| `1 ) by A3, EUCLID: 55

      .= (((1 - lambda) * (p1 `1 )) + (lambda * (p2 `1 ))) by A6, A7, EUCLID: 52;

      (lambda * (p1 `1 )) <= (lambda * (p2 `1 )) by A1, A4, XREAL_1: 64;

      then (((1 - lambda) * (p1 `1 )) + (lambda * (p1 `1 ))) <= (p `1 ) by A8, XREAL_1: 7;

      hence (p1 `1 ) <= (p `1 );

       0 <= (1 - lambda) by A5, XREAL_1: 48;

      then ((1 - lambda) * (p1 `1 )) <= ((1 - lambda) * (p2 `1 )) by A1, XREAL_1: 64;

      then (p `1 ) <= (((1 - lambda) * (p2 `1 )) + (lambda * (p2 `1 ))) by A8, XREAL_1: 6;

      hence thesis;

    end;

    theorem :: TOPREAL1:4

    (p1 `2 ) <= (p2 `2 ) & p in ( LSeg (p1,p2)) implies (p1 `2 ) <= (p `2 ) & (p `2 ) <= (p2 `2 )

    proof

      assume that

       A1: (p1 `2 ) <= (p2 `2 ) and

       A2: p in ( LSeg (p1,p2));

      consider lambda such that

       A3: p = (((1 - lambda) * p1) + (lambda * p2)) and

       A4: 0 <= lambda and

       A5: lambda <= 1 by A2;

      

       A6: (((1 - lambda) * p1) `2 ) = ( |[((1 - lambda) * (p1 `1 )), ((1 - lambda) * (p1 `2 ))]| `2 ) by EUCLID: 57

      .= ((1 - lambda) * (p1 `2 )) by EUCLID: 52;

      

       A7: ((lambda * p2) `2 ) = ( |[(lambda * (p2 `1 )), (lambda * (p2 `2 ))]| `2 ) by EUCLID: 57

      .= (lambda * (p2 `2 )) by EUCLID: 52;

      

       A8: (p `2 ) = ( |[((((1 - lambda) * p1) `1 ) + ((lambda * p2) `1 )), ((((1 - lambda) * p1) `2 ) + ((lambda * p2) `2 ))]| `2 ) by A3, EUCLID: 55

      .= (((1 - lambda) * (p1 `2 )) + (lambda * (p2 `2 ))) by A6, A7, EUCLID: 52;

      (lambda * (p1 `2 )) <= (lambda * (p2 `2 )) by A1, A4, XREAL_1: 64;

      then (((1 - lambda) * (p1 `2 )) + (lambda * (p1 `2 ))) <= (p `2 ) by A8, XREAL_1: 7;

      hence (p1 `2 ) <= (p `2 );

       0 <= (1 - lambda) by A5, XREAL_1: 48;

      then ((1 - lambda) * (p1 `2 )) <= ((1 - lambda) * (p2 `2 )) by A1, XREAL_1: 64;

      then (p `2 ) <= (((1 - lambda) * (p2 `2 )) + (lambda * (p2 `2 ))) by A8, XREAL_1: 6;

      hence thesis;

    end;

    theorem :: TOPREAL1:5

    

     Th5: for p,p1,p2 be Point of ( TOP-REAL n) st p in ( LSeg (p1,p2)) holds ( LSeg (p1,p2)) = (( LSeg (p1,p)) \/ ( LSeg (p,p2)))

    proof

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

      now

        assume

         A1: p in ( LSeg (p1,p2));

        then

        consider r such that

         A2: p = (((1 - r) * p1) + (r * p2)) and

         A3: 0 <= r and

         A4: r <= 1;

        now

          per cases ;

            suppose

             A5: 0 <> r & r <> 1;

            now

              let q be object;

              assume q in ( LSeg (p1,p2));

              then

              consider b be Real such that

               A6: q = (((1 - b) * p1) + (b * p2)) and

               A7: 0 <= b and

               A8: b <= 1;

              now

                per cases ;

                  suppose

                   A9: b <= r;

                  set x = (b * (1 / r));

                  x <= (r * (1 / r)) by A3, A9, XREAL_1: 64;

                  then

                   A10: x <= 1 by A5, XCMPLX_1: 106;

                  (((1 - x) * p1) + (x * p)) = (((1 - x) * p1) + ((x * ((1 - r) * p1)) + (x * (r * p2)))) by A2, RLVECT_1:def 5

                  .= ((((1 - x) * p1) + (x * ((1 - r) * p1))) + (x * (r * p2))) by RLVECT_1:def 3

                  .= ((((1 - x) * p1) + ((x * (1 - r)) * p1)) + (x * (r * p2))) by RLVECT_1:def 7

                  .= ((((1 - x) * p1) + ((x * (1 - r)) * p1)) + ((x * r) * p2)) by RLVECT_1:def 7

                  .= ((((1 - x) + (x * (1 - r))) * p1) + ((x * r) * p2)) by RLVECT_1:def 6

                  .= (((1 - (x * r)) * p1) + (b * p2)) by A5, XCMPLX_1: 109

                  .= q by A5, A6, XCMPLX_1: 109;

                  then q in { (((1 - lambda) * p1) + (lambda * p)) : 0 <= lambda & lambda <= 1 } by A3, A7, A10;

                  hence q in (( LSeg (p1,p)) \/ ( LSeg (p,p2))) by XBOOLE_0:def 3;

                end;

                  suppose

                   A11: not b <= r;

                  set bp = (1 - b), rp = (1 - r);

                  set x = (bp * (1 / rp));

                  

                   A12: 0 <> rp by A5;

                  (r - r) = 0 ;

                  then

                   A13: 0 <= rp by A4, XREAL_1: 9;

                  bp <= rp by A11, XREAL_1: 10;

                  then x <= (rp * (1 / rp)) by A13, XREAL_1: 64;

                  then

                   A14: x <= 1 by A12, XCMPLX_1: 106;

                  

                   A15: 0 <= bp by A8, XREAL_1: 48;

                  

                   A16: (1 - 0 ) = 1;

                  (((1 - x) * p2) + (x * p)) = (((1 - x) * p2) + ((x * ((1 - rp) * p2)) + (x * (rp * p1)))) by A2, RLVECT_1:def 5

                  .= ((((1 - x) * p2) + (x * ((1 - rp) * p2))) + (x * (rp * p1))) by RLVECT_1:def 3

                  .= ((((1 - x) * p2) + ((x * (1 - rp)) * p2)) + (x * (rp * p1))) by RLVECT_1:def 7

                  .= ((((1 - x) * p2) + ((x * (1 - rp)) * p2)) + ((x * rp) * p1)) by RLVECT_1:def 7

                  .= ((((1 - x) + (x * (1 - rp))) * p2) + ((x * rp) * p1)) by RLVECT_1:def 6

                  .= (((1 - (x * rp)) * p2) + (bp * p1)) by A5, A16, XCMPLX_1: 109

                  .= (((1 - bp) * p2) + (bp * p1)) by A12, XCMPLX_1: 109

                  .= q by A6;

                  then q in { (((1 - lambda) * p2) + (lambda * p)) : 0 <= lambda & lambda <= 1 } by A15, A13, A14;

                  then q in ( LSeg (p,p2)) by RLTOPSP1:def 2;

                  hence q in (( LSeg (p1,p)) \/ ( LSeg (p,p2))) by XBOOLE_0:def 3;

                end;

              end;

              hence q in (( LSeg (p1,p)) \/ ( LSeg (p,p2)));

            end;

            then

             A17: ( LSeg (p1,p2)) c= (( LSeg (p1,p)) \/ ( LSeg (p,p2)));

            

             A18: ( LSeg (p,p2)) c= ( LSeg (p1,p2)) by A1, Lm1;

            ( LSeg (p1,p)) c= ( LSeg (p1,p2)) by A1, Lm1;

            then (( LSeg (p1,p)) \/ ( LSeg (p,p2))) c= ( LSeg (p1,p2)) by A18, XBOOLE_1: 8;

            hence thesis by A17;

          end;

            suppose

             A19: not ( 0 <> r & r <> 1);

            now

              per cases by A19;

                suppose

                 A20: r = 0 ;

                

                 A21: p in ( LSeg (p,p2)) by RLTOPSP1: 68;

                

                 A22: p = ((1 * p1) + ( 0. ( TOP-REAL n))) by A2, A20, RLVECT_1: 10

                .= (p1 + ( 0. ( TOP-REAL n))) by RLVECT_1:def 8

                .= p1 by RLVECT_1: 4;

                then ( LSeg (p1,p)) = {p} by RLTOPSP1: 70;

                then ( LSeg (p1,p)) c= ( LSeg (p,p2)) by A21, ZFMISC_1: 31;

                hence ( LSeg (p1,p2)) = (( LSeg (p1,p)) \/ ( LSeg (p,p2))) by A22, XBOOLE_1: 12;

              end;

                suppose

                 A23: r = 1;

                

                 A24: p in ( LSeg (p1,p)) by RLTOPSP1: 68;

                

                 A25: p = (( 0. ( TOP-REAL n)) + (1 * p2)) by A2, A23, RLVECT_1: 10

                .= (( 0. ( TOP-REAL n)) + p2) by RLVECT_1:def 8

                .= p2 by RLVECT_1: 4;

                then ( LSeg (p,p2)) = {p} by RLTOPSP1: 70;

                then ( LSeg (p,p2)) c= ( LSeg (p1,p)) by A24, ZFMISC_1: 31;

                hence ( LSeg (p1,p2)) = (( LSeg (p1,p)) \/ ( LSeg (p,p2))) by A25, XBOOLE_1: 12;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL1:6

    

     Th6: for p1,p2,q1,q2 be Point of ( TOP-REAL n) st q1 in ( LSeg (p1,p2)) & q2 in ( LSeg (p1,p2)) holds ( LSeg (q1,q2)) c= ( LSeg (p1,p2))

    proof

      let p1,p2,q1,q2 be Point of ( TOP-REAL n);

      assume that

       A1: q1 in ( LSeg (p1,p2)) and

       A2: q2 in ( LSeg (p1,p2));

      

       A3: ( LSeg (p1,p2)) = (( LSeg (p1,q1)) \/ ( LSeg (q1,p2))) by A1, Th5;

      now

        per cases by A2, A3, XBOOLE_0:def 3;

          suppose

           A4: q2 in ( LSeg (p1,q1));

          

           A5: ( LSeg (p1,q1)) c= ( LSeg (p1,p2)) by A1, Lm1;

          ( LSeg (q2,q1)) c= ( LSeg (p1,q1)) by A4, Lm1;

          hence thesis by A5;

        end;

          suppose

           A6: q2 in ( LSeg (q1,p2));

          

           A7: ( LSeg (q1,p2)) c= ( LSeg (p1,p2)) by A1, Lm1;

          ( LSeg (q1,q2)) c= ( LSeg (q1,p2)) by A6, Lm1;

          hence thesis by A7;

        end;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL1:7

    for p,q,p1,p2 be Point of ( TOP-REAL n) st p in ( LSeg (p1,p2)) & q in ( LSeg (p1,p2)) holds ( LSeg (p1,p2)) = ((( LSeg (p1,p)) \/ ( LSeg (p,q))) \/ ( LSeg (q,p2)))

    proof

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

      assume that

       A1: p in ( LSeg (p1,p2)) and

       A2: q in ( LSeg (p1,p2));

      

       A3: ( LSeg (p,q)) c= ( LSeg (p1,p2)) by A1, A2, Th6;

      

       A4: ( LSeg (p1,p2)) = (( LSeg (p1,q)) \/ ( LSeg (q,p2))) by A2, Th5;

       A5:

      now

        per cases ;

          suppose p in ( LSeg (p1,q));

          hence ( LSeg (p1,p2)) c= ((( LSeg (p1,p)) \/ ( LSeg (p,q))) \/ ( LSeg (q,p2))) by A4, Th5;

        end;

          suppose not p in ( LSeg (p1,q));

          then p in ( LSeg (q,p2)) by A1, A4, XBOOLE_0:def 3;

          then

           A6: ( LSeg (q,p2)) = (( LSeg (q,p)) \/ ( LSeg (p,p2))) by Th5;

          ( LSeg (p1,p2)) = (( LSeg (p1,p)) \/ ( LSeg (p,p2))) by A1, Th5;

          then

           A7: ( LSeg (p1,p2)) c= (( LSeg (p1,p)) \/ ( LSeg (q,p2))) by A6, XBOOLE_1: 7, XBOOLE_1: 9;

          

           A8: ((( LSeg (p1,p)) \/ ( LSeg (q,p2))) \/ ( LSeg (p,q))) = ((( LSeg (p1,p)) \/ ( LSeg (p,q))) \/ ( LSeg (q,p2))) by XBOOLE_1: 4;

          (( LSeg (p1,p)) \/ ( LSeg (q,p2))) c= ((( LSeg (p1,p)) \/ ( LSeg (q,p2))) \/ ( LSeg (p,q))) by XBOOLE_1: 7;

          hence ( LSeg (p1,p2)) c= ((( LSeg (p1,p)) \/ ( LSeg (p,q))) \/ ( LSeg (q,p2))) by A7, A8;

        end;

      end;

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

      then ( LSeg (p1,p)) c= ( LSeg (p1,p2)) by A1, Th6;

      then

       A9: (( LSeg (p1,p)) \/ ( LSeg (p,q))) c= ( LSeg (p1,p2)) by A3, XBOOLE_1: 8;

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

      then ( LSeg (q,p2)) c= ( LSeg (p1,p2)) by A2, Th6;

      then ((( LSeg (p1,p)) \/ ( LSeg (p,q))) \/ ( LSeg (q,p2))) c= ( LSeg (p1,p2)) by A9, XBOOLE_1: 8;

      hence thesis by A5;

    end;

    theorem :: TOPREAL1:8

    for p,p1,p2 be Point of ( TOP-REAL n) st p in ( LSeg (p1,p2)) holds (( LSeg (p1,p)) /\ ( LSeg (p,p2))) = {p}

    proof

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

      

       A1: p in ( LSeg (p,p2)) by RLTOPSP1: 68;

      assume

       A2: p in ( LSeg (p1,p2));

       A3:

      now

        assume not (( LSeg (p1,p)) /\ ( LSeg (p,p2))) c= {p};

        then

        consider y be object such that

         A4: y in (( LSeg (p1,p)) /\ ( LSeg (p,p2))) and

         A5: not y in {p};

        reconsider q = y as Point of ( TOP-REAL n) by A4;

        

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

        then

        consider d be Real such that

         A7: q = (((1 - d) * p1) + (d * p)) and 0 <= d and

         A8: d <= 1;

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

        then

        consider e be Real such that

         A9: q = (((1 - e) * p) + (e * p2)) and

         A10: 0 <= e and e <= 1;

        consider a be Real such that

         A11: p = (((1 - a) * p1) + (a * p2)) and

         A12: 0 <= a and

         A13: a <= 1 by A2;

        

         A14: (1 - a) >= 0 by A13, XREAL_1: 48;

        now

          assume d = 1;

          

          then q = (((1 - 1) * p1) + p) by A7, RLVECT_1:def 8

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

          .= p by RLVECT_1: 4;

          hence contradiction by A5, TARSKI:def 1;

        end;

        then d < 1 by A8, XXREAL_0: 1;

        then

         A15: (1 - d) > 0 by XREAL_1: 50;

        now

          assume a = 0 ;

          

          then p = (((1 - 0 ) * p1) + ( 0. ( TOP-REAL n))) by A11, RLVECT_1: 10

          .= ((1 - 0 ) * p1) by RLVECT_1: 4

          .= p1 by RLVECT_1:def 8;

          hence contradiction by A5, A6, RLTOPSP1: 70;

        end;

        then

         A16: ((1 - d) * a) > 0 by A12, A15, XREAL_1: 129;

        set f = (((1 - e) * a) + e);

        q = ((((1 - e) * ((1 - a) * p1)) + ((1 - e) * (a * p2))) + (e * p2)) by A11, A9, RLVECT_1:def 5

        .= (((((1 - e) * (1 - a)) * p1) + ((1 - e) * (a * p2))) + (e * p2)) by RLVECT_1:def 7

        .= (((((1 - e) * (1 - a)) * p1) + (((1 - e) * a) * p2)) + (e * p2)) by RLVECT_1:def 7

        .= ((((1 - e) * (1 - a)) * p1) + ((((1 - e) * a) * p2) + (e * p2))) by RLVECT_1:def 3

        .= ((((1 - e) * (1 - a)) * p1) + ((((1 - e) * a) + e) * p2)) by RLVECT_1:def 6;

        

        then

         A17: (p - q) = (((((1 - a) * p1) + (a * p2)) - ((1 - f) * p1)) - (f * p2)) by A11, RLVECT_1: 27

        .= (((((1 - a) * p1) - ((1 - f) * p1)) + (a * p2)) - (f * p2)) by RLVECT_1:def 3

        .= (((((1 - a) - (1 - f)) * p1) + (a * p2)) - (f * p2)) by RLVECT_1: 35

        .= ((((f - a) * p1) - (f * p2)) + (a * p2)) by RLVECT_1:def 3

        .= (((f - a) * p1) - ((f * p2) - (a * p2))) by RLVECT_1: 29

        .= (((f - a) * p1) - ((f - a) * p2)) by RLVECT_1: 35

        .= ((f - a) * (p1 - p2)) by RLVECT_1: 34;

        q = (((1 - d) * p1) + ((d * ((1 - a) * p1)) + (d * (a * p2)))) by A11, A7, RLVECT_1:def 5

        .= ((((1 - d) * p1) + (d * ((1 - a) * p1))) + (d * (a * p2))) by RLVECT_1:def 3

        .= ((((1 - d) * p1) + ((d * (1 - a)) * p1)) + (d * (a * p2))) by RLVECT_1:def 7

        .= ((((1 - d) + (d * (1 - a))) * p1) + (d * (a * p2))) by RLVECT_1:def 6

        .= (((1 - (d * a)) * p1) + ((d * a) * p2)) by RLVECT_1:def 7;

        

        then (p - q) = (((((1 - a) * p1) + (a * p2)) - ((1 - (d * a)) * p1)) - ((d * a) * p2)) by A11, RLVECT_1: 27

        .= (((((1 - a) * p1) - ((1 - (d * a)) * p1)) + (a * p2)) - ((d * a) * p2)) by RLVECT_1:def 3

        .= (((((1 - a) - (1 - (d * a))) * p1) + (a * p2)) - ((d * a) * p2)) by RLVECT_1: 35

        .= (((((d * a) - a) * p1) - ((d * a) * p2)) + (a * p2)) by RLVECT_1:def 3

        .= ((((d * a) - a) * p1) - (((d * a) * p2) - (a * p2))) by RLVECT_1: 29

        .= ((((d * a) - a) * p1) - (((d * a) - a) * p2)) by RLVECT_1: 35

        .= (((d * a) - a) * (p1 - p2)) by RLVECT_1: 34;

        then (((f - a) * (p1 - p2)) - (((d * a) - a) * (p1 - p2))) = ( 0. ( TOP-REAL n)) by A17, RLVECT_1: 5;

        then (((f - a) - ((d * a) - a)) * (p1 - p2)) = ( 0. ( TOP-REAL n)) by RLVECT_1: 35;

        then

         A18: (f - (d * a)) = 0 or (p1 - p2) = ( 0. ( TOP-REAL n)) by RLVECT_1: 11;

        ((((1 - e) * a) + e) - (d * a)) = (((1 - d) * a) + (e * (1 - a)));

        then p1 = p2 by A10, A18, A16, A14, RLVECT_1: 21;

        then p in {p1} by A2, RLTOPSP1: 70;

        then p = p1 by TARSKI:def 1;

        hence contradiction by A5, A6, RLTOPSP1: 70;

      end;

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

      then p in (( LSeg (p1,p)) /\ ( LSeg (p,p2))) by A1, XBOOLE_0:def 4;

      then {p} c= (( LSeg (p1,p)) /\ ( LSeg (p,p2))) by ZFMISC_1: 31;

      hence thesis by A3;

    end;

    

     Lm2: for T be TopSpace holds T is T_2 iff the TopStruct of T is T_2

    proof

      let T be TopSpace;

      thus T is T_2 implies the TopStruct of T is T_2

      proof

        assume

         A1: T is T_2;

        let p,q be Point of the TopStruct of T such that

         A2: p <> q;

        reconsider pp = p, qq = q as Point of T;

        consider G1,G2 be Subset of T such that

         A3: G1 is open and

         A4: G2 is open and

         A5: pp in G1 and

         A6: qq in G2 and

         A7: G1 misses G2 by A1, A2;

        reconsider H1 = G1, H2 = G2 as Subset of the TopStruct of T;

        take H1, H2;

        thus H1 is open & H2 is open by A3, A4;

        thus p in H1 & q in H2 & H1 misses H2 by A5, A6, A7;

      end;

      assume

       A8: the TopStruct of T is T_2;

      let p,q be Point of T such that

       A9: p <> q;

      reconsider pp = p, qq = q as Point of the TopStruct of T;

      consider G1,G2 be Subset of the TopStruct of T such that

       A10: G1 is open and

       A11: G2 is open and

       A12: pp in G1 and

       A13: qq in G2 and

       A14: G1 misses G2 by A8, A9;

      reconsider H1 = G1, H2 = G2 as Subset of T;

      take H1, H2;

      thus H1 is open & H2 is open by A10, A11;

      thus p in H1 & q in H2 & H1 misses H2 by A12, A13, A14;

    end;

    registration

      let n;

      cluster the carrier of ( TOP-REAL n) -> functional;

      coherence by EUCLID: 23;

    end

    theorem :: TOPREAL1:9

    

     Th9: for p1,p2 be Point of ( TOP-REAL n) st p1 <> p2 holds ( LSeg (p1,p2)) is_an_arc_of (p1,p2)

    proof

      let p1,p2 be Point of ( TOP-REAL n);

      set P = ( LSeg (p1,p2));

      reconsider PP = P as Subset of ( Euclid n) by EUCLID: 67;

      PP is non empty;

      then

      reconsider PP = P as non empty Subset of ( Euclid n);

      reconsider p19 = p1, p29 = p2 as Element of ( REAL n) by EUCLID: 22;

      defpred X[ object, object] means for x be Real st x = $1 holds $2 = (((1 - x) * p1) + (x * p2));

      

       A1: for a be object st a in [. 0 , 1.] holds ex u be object st X[a, u]

      proof

        let a be object;

        assume a in [. 0 , 1.];

        then

        reconsider x = a as Real;

        take (((1 - x) * p1) + (x * p2));

        thus thesis;

      end;

      consider f be Function such that

       A2: ( dom f) = [. 0 , 1.] and

       A3: for a be object st a in [. 0 , 1.] holds X[a, (f . a)] from CLASSES1:sch 1( A1);

      

       A4: ( rng f) c= the carrier of (( TOP-REAL n) | P)

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A5: x in ( dom f) and

         A6: y = (f . x) by FUNCT_1:def 3;

        x in { r : 0 <= r & r <= 1 } by A2, A5, RCOMP_1:def 1;

        then

        consider r such that

         A7: r = x and

         A8: 0 <= r and

         A9: r <= 1;

        y = (((1 - r) * p1) + (r * p2)) by A2, A3, A5, A6, A7;

        then y in { (((1 - lambda) * p1) + (lambda * p2)) : 0 <= lambda & lambda <= 1 } by A8, A9;

        then y in ( [#] (( TOP-REAL n) | P)) by PRE_TOPC:def 5;

        hence thesis;

      end;

      then

      reconsider f as Function of I[01] , (( TOP-REAL n) | P) by A2, BORSUK_1: 40, FUNCT_2:def 1, RELSET_1: 4;

      

       A10: I[01] is compact by HEINE: 4, TOPMETR: 20;

      assume

       A11: p1 <> p2;

      now

        let x1,x2 be object;

        assume that

         A12: x1 in ( dom f) and

         A13: x2 in ( dom f) and

         A14: (f . x1) = (f . x2);

        x2 in { r : 0 <= r & r <= 1 } by A2, A13, RCOMP_1:def 1;

        then

        consider r2 be Real such that

         A15: r2 = x2 and 0 <= r2 and r2 <= 1;

        

         A16: (f . x2) = (((1 - r2) * p1) + (r2 * p2)) by A2, A3, A13, A15;

        x1 in { r : 0 <= r & r <= 1 } by A2, A12, RCOMP_1:def 1;

        then

        consider r1 be Real such that

         A17: r1 = x1 and 0 <= r1 and r1 <= 1;

        (f . x1) = (((1 - r1) * p1) + (r1 * p2)) by A2, A3, A12, A17;

        then ((((1 - r1) * p1) + (r1 * p2)) + (( - r1) * p2)) = (((1 - r2) * p1) + ((r2 * p2) + (( - r1) * p2))) by A14, A16, RLVECT_1:def 3;

        then ((((1 - r1) * p1) + (r1 * p2)) + (( - r1) * p2)) = (((1 - r2) * p1) + ((r2 + ( - r1)) * p2)) by RLVECT_1:def 6;

        then (((1 - r1) * p1) + ((r1 * p2) + (( - r1) * p2))) = (((1 - r2) * p1) + ((r2 - r1) * p2)) by RLVECT_1:def 3;

        then (((1 - r1) * p1) + ((r1 + ( - r1)) * p2)) = (((1 - r2) * p1) + ((r2 - r1) * p2)) by RLVECT_1:def 6;

        then (((1 - r1) * p1) + ( 0. ( TOP-REAL n))) = (((1 - r2) * p1) + ((r2 - r1) * p2)) by RLVECT_1: 10;

        then ((( - (1 - r2)) * p1) + ((1 - r1) * p1)) = ((( - (1 - r2)) * p1) + (((1 - r2) * p1) + ((r2 - r1) * p2))) by RLVECT_1: 4;

        then ((( - (1 - r2)) * p1) + ((1 - r1) * p1)) = (((( - (1 - r2)) * p1) + ((1 - r2) * p1)) + ((r2 - r1) * p2)) by RLVECT_1:def 3;

        then ((( - (1 - r2)) * p1) + ((1 - r1) * p1)) = (((( - (1 - r2)) + (1 - r2)) * p1) + ((r2 - r1) * p2)) by RLVECT_1:def 6;

        then ((( - (1 - r2)) * p1) + ((1 - r1) * p1)) = (( 0. ( TOP-REAL n)) + ((r2 - r1) * p2)) by RLVECT_1: 10;

        then ((( - (1 - r2)) * p1) + ((1 - r1) * p1)) = ((r2 - r1) * p2) by RLVECT_1: 4;

        then (((r2 - 1) + (1 - r1)) * p1) = ((r2 - r1) * p2) by RLVECT_1:def 6;

        then (r2 - r1) = 0 by A11, RLVECT_1: 36;

        hence x1 = x2 by A17, A15;

      end;

      then

       A18: f is one-to-one;

      ( [#] (( TOP-REAL n) | P)) c= ( rng f)

      proof

        let a be object;

        assume a in ( [#] (( TOP-REAL n) | P));

        then a in P by PRE_TOPC:def 5;

        then

        consider lambda such that

         A19: a = (((1 - lambda) * p1) + (lambda * p2)) and

         A20: 0 <= lambda and

         A21: lambda <= 1;

        lambda in { r : 0 <= r & r <= 1 } by A20, A21;

        then

         A22: lambda in ( dom f) by A2, RCOMP_1:def 1;

        then a = (f . lambda) by A2, A3, A19;

        hence thesis by A22, FUNCT_1:def 3;

      end;

      then

       A23: ( rng f) = ( [#] (( TOP-REAL n) | P)) by A4;

      

       A24: ( TopSpaceMetr ( Euclid n)) is T_2 by PCOMPS_1: 34;

      

       A25: (( TOP-REAL n) | P) = ( TopSpaceMetr (( Euclid n) | PP)) by EUCLID: 63;

      for W be Point of I[01] , G be a_neighborhood of (f . W) holds ex H be a_neighborhood of W st (f .: H) c= G

      proof

        reconsider p11 = p1, p22 = p2 as Point of ( Euclid n) by EUCLID: 67;

        let W be Point of I[01] , G be a_neighborhood of (f . W);

        reconsider W9 = W as Point of ( Closed-Interval-MSpace ( 0 ,1)) by BORSUK_1: 40, TOPMETR: 10;

        

         A26: (( Pitag_dist n) . (p19,p29)) = ( dist (p11,p22)) by METRIC_1:def 1;

        ( [#] (( TOP-REAL n) | P)) = P by PRE_TOPC:def 5;

        then

        reconsider Y = (f . W) as Point of (( Euclid n) | PP) by TOPMETR:def 2;

        

         A27: ( dist (p11,p22)) >= 0 by METRIC_1: 5;

        reconsider W1 = W as Real;

        P = the carrier of (( Euclid n) | PP) by TOPMETR:def 2;

        then

        reconsider WW9 = Y as Point of ( Euclid n) by TARSKI:def 3;

        (f . W) in ( Int G) by CONNSP_2:def 1;

        then

        consider Q be Subset of (( TOP-REAL n) | P) such that

         A28: Q is open and

         A29: Q c= G and

         A30: (f . W) in Q by TOPS_1: 22;

        consider r be Real such that

         A31: r > 0 and

         A32: ( Ball (Y,r)) c= Q by A25, A28, A30, TOPMETR: 15;

        reconsider r as Element of REAL by XREAL_0:def 1;

        set delta = (r / (( Pitag_dist n) . (p19,p29)));

        reconsider H = ( Ball (W9,delta)) as Subset of I[01] by BORSUK_1: 40, TOPMETR: 10;

        ( Closed-Interval-TSpace ( 0 ,1)) = ( TopSpaceMetr ( Closed-Interval-MSpace ( 0 ,1))) by TOPMETR:def 7;

        then

         A33: H is open by TOPMETR: 14, TOPMETR: 20;

        

         A34: ( dist (p11,p22)) <> 0 by A11, METRIC_1: 2;

        then W in H by A31, A26, A27, TBSP_1: 11, XREAL_1: 139;

        then W in ( Int H) by A33, TOPS_1: 23;

        then

        reconsider H as a_neighborhood of W by CONNSP_2:def 1;

        take H;

        

         A35: delta > 0 by A31, A26, A27, A34, XREAL_1: 139;

        (f .: H) c= ( Ball (Y,r))

        proof

          reconsider WW1 = WW9 as Element of ( REAL n);

          let a be object;

          

           A36: ( rng f) c= the carrier of (( TOP-REAL n) | P) by RELAT_1:def 19;

          assume a in (f .: H);

          then

          consider u be object such that

           A37: u in ( dom f) and

           A38: u in H and

           A39: a = (f . u) by FUNCT_1:def 6;

          reconsider u1 = u as Real by A2, A37;

          

           A40: ( [#] (( TOP-REAL n) | P)) = P by PRE_TOPC:def 5;

          reconsider u9 = u as Point of ( Closed-Interval-MSpace ( 0 ,1)) by A38;

          reconsider W99 = W9, u99 = u9 as Point of RealSpace by TOPMETR: 8;

          

           A41: ( dist (W9,u9)) = (the distance of ( Closed-Interval-MSpace ( 0 ,1)) . (W9,u9)) by METRIC_1:def 1

          .= (the distance of RealSpace . (W99,u99)) by TOPMETR:def 1

          .= ( dist (W99,u99)) by METRIC_1:def 1;

          ( dist (W9,u9)) < delta by A38, METRIC_1: 11;

          then |.(W1 - u1).| < delta by A41, TOPMETR: 11;

          then |.( - (u1 - W1)).| < delta;

          then

           A42: |.(u1 - W1).| < delta by COMPLEX1: 52;

          

           A43: delta <> 0 by A31, A26, A27, A34, XREAL_1: 139;

          then (( Pitag_dist n) . (p19,p29)) = (r / delta) by XCMPLX_1: 54;

          then

           A44: |.(p19 - p29).| = (r / delta) by EUCLID:def 6;

          (f . u) in ( rng f) by A37, FUNCT_1:def 3;

          then

          reconsider aa = a as Point of (( Euclid n) | PP) by A39, A36, A40, TOPMETR:def 2;

          P = the carrier of (( Euclid n) | PP) by TOPMETR:def 2;

          then

          reconsider aa9 = aa as Point of ( Euclid n) by TARSKI:def 3;

          reconsider aa1 = aa9 as Element of ( REAL n);

          

           A45: (p19 - p29) = (p1 - p2) by EUCLID: 69;

          

           A46: WW1 = (((1 - W1) * p1) + (W1 * p2)) by A3, BORSUK_1: 40;

          aa1 = (((1 - u1) * p1) + (u1 * p2)) by A2, A3, A37, A39;

          

          then (WW1 - aa1) = ((((1 - W1) * p1) + (W1 * p2)) - (((1 - u1) * p1) + (u1 * p2))) by A46, EUCLID: 69

          .= ((((W1 * p2) + ((1 - W1) * p1)) - ((1 - u1) * p1)) - (u1 * p2)) by RLVECT_1: 27

          .= (((W1 * p2) + (((1 - W1) * p1) - ((1 - u1) * p1))) - (u1 * p2)) by RLVECT_1:def 3

          .= (((W1 * p2) + (((1 - W1) - (1 - u1)) * p1)) - (u1 * p2)) by RLVECT_1: 35

          .= (((u1 - W1) * p1) + ((W1 * p2) - (u1 * p2))) by RLVECT_1:def 3

          .= (((u1 - W1) * p1) + ((W1 - u1) * p2)) by RLVECT_1: 35

          .= (((u1 - W1) * p1) + (( - (u1 - W1)) * p2))

          .= (((u1 - W1) * p1) + ( - ((u1 - W1) * p2))) by RLVECT_1: 79

          .= (((u1 - W1) * p1) - ((u1 - W1) * p2))

          .= ((u1 - W1) * (p1 - p2)) by RLVECT_1: 34

          .= ((u1 - W1) * (p19 - p29)) by A45, EUCLID: 65;

          then

           A47: |.(WW1 - aa1).| = ( |.(u1 - W1).| * |.(p19 - p29).|) by EUCLID: 11;

          (r / delta) > 0 by A31, A35, XREAL_1: 139;

          then |.(WW1 - aa1).| < (delta * (r / delta)) by A47, A42, A44, XREAL_1: 68;

          then |.(WW1 - aa1).| < r by A43, XCMPLX_1: 87;

          then (the distance of ( Euclid n) . (WW9,aa9)) < r by EUCLID:def 6;

          then (the distance of (( Euclid n) | PP) . (Y,aa)) < r by TOPMETR:def 1;

          then ( dist (Y,aa)) < r by METRIC_1:def 1;

          hence thesis by METRIC_1: 11;

        end;

        then (f .: H) c= Q by A32;

        hence thesis by A29;

      end;

      then

       A48: f is continuous by BORSUK_1:def 1;

      take f;

      

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

      then

      reconsider PP = P as Subset of ( TopSpaceMetr ( Euclid n));

      (( TopSpaceMetr ( Euclid n)) | PP) = (( TOP-REAL n) | P) by A49, PRE_TOPC: 36;

      then (( TOP-REAL n) | P) is T_2 by A24, TOPMETR: 2;

      hence f is being_homeomorphism by A23, A18, A48, A10, COMPTS_1: 17;

       0 in [. 0 , 1.] by XXREAL_1: 1;

      

      hence (f . 0 ) = (((1 - 0 ) * p1) + ( 0 * p2)) by A3

      .= (p1 + ( 0 * p2)) by RLVECT_1:def 8

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

      .= p1 by RLVECT_1: 4;

      1 in [. 0 , 1.] by XXREAL_1: 1;

      

      hence (f . 1) = (((1 - 1) * p1) + (1 * p2)) by A3

      .= (( 0. ( TOP-REAL n)) + (1 * p2)) by RLVECT_1: 10

      .= (1 * p2) by RLVECT_1: 4

      .= p2 by RLVECT_1:def 8;

    end;

    registration

      let n;

      cluster ( TOP-REAL n) -> T_2;

      coherence

      proof

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

        then the TopStruct of ( TOP-REAL n) is T_2 by PCOMPS_1: 34;

        hence thesis by Lm2;

      end;

    end

    theorem :: TOPREAL1:10

    

     Th10: for P be Subset of ( TOP-REAL n), p1,p2,q1 be Point of ( TOP-REAL n) st P is_an_arc_of (p1,p2) & (P /\ ( LSeg (p2,q1))) = {p2} holds (P \/ ( LSeg (p2,q1))) is_an_arc_of (p1,q1)

    proof

      let P be Subset of ( TOP-REAL n), p1,p2,q1 be Point of ( TOP-REAL n);

      assume that

       A1: P is_an_arc_of (p1,p2) and

       A2: (P /\ ( LSeg (p2,q1))) = {p2};

      per cases ;

        suppose p2 <> q1;

        then ( LSeg (p2,q1)) is_an_arc_of (p2,q1) by Th9;

        hence thesis by A1, A2, Th2;

      end;

        suppose

         A3: p2 = q1;

        then

         A4: ( LSeg (p2,q1)) = {q1} by RLTOPSP1: 70;

        q1 in P by A1, A3, Th1;

        hence thesis by A1, A3, A4, ZFMISC_1: 40;

      end;

    end;

    theorem :: TOPREAL1:11

    

     Th11: for P be Subset of ( TOP-REAL n), p1,p2,q1 be Point of ( TOP-REAL n) st P is_an_arc_of (p2,p1) & (( LSeg (q1,p2)) /\ P) = {p2} holds (( LSeg (q1,p2)) \/ P) is_an_arc_of (q1,p1)

    proof

      let P be Subset of ( TOP-REAL n), p1,p2,q1 be Point of ( TOP-REAL n);

      assume that

       A1: P is_an_arc_of (p2,p1) and

       A2: (( LSeg (q1,p2)) /\ P) = {p2};

      per cases ;

        suppose p2 <> q1;

        then ( LSeg (q1,p2)) is_an_arc_of (q1,p2) by Th9;

        hence thesis by A1, A2, Th2;

      end;

        suppose

         A3: p2 = q1;

        then

         A4: ( LSeg (q1,p2)) = {q1} by RLTOPSP1: 70;

        q1 in P by A1, A3, Th1;

        hence thesis by A1, A3, A4, ZFMISC_1: 40;

      end;

    end;

    theorem :: TOPREAL1:12

    for p1,p2,q1 be Point of ( TOP-REAL n) st (p1 <> p2 or p2 <> q1) & (( LSeg (p1,p2)) /\ ( LSeg (p2,q1))) = {p2} holds (( LSeg (p1,p2)) \/ ( LSeg (p2,q1))) is_an_arc_of (p1,q1)

    proof

      let p1,p2,q1 be Point of ( TOP-REAL n);

      assume that

       A1: p1 <> p2 or p2 <> q1 and

       A2: (( LSeg (p1,p2)) /\ ( LSeg (p2,q1))) = {p2};

      per cases by A1;

        suppose p1 <> p2;

        hence thesis by A2, Th9, Th10;

      end;

        suppose p2 <> q1;

        hence thesis by A2, Th9, Th11;

      end;

    end;

    theorem :: TOPREAL1:13

    

     Th13: ( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) = { p1 : (p1 `1 ) = 0 & (p1 `2 ) <= 1 & (p1 `2 ) >= 0 } & ( LSeg ( |[ 0 , 1]|, |[1, 1]|)) = { p2 : (p2 `1 ) <= 1 & (p2 `1 ) >= 0 & (p2 `2 ) = 1 } & ( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) = { q1 : (q1 `1 ) <= 1 & (q1 `1 ) >= 0 & (q1 `2 ) = 0 } & ( LSeg ( |[1, 0 ]|, |[1, 1]|)) = { q2 : (q2 `1 ) = 1 & (q2 `2 ) <= 1 & (q2 `2 ) >= 0 }

    proof

      set p0 = |[ 0 , 0 ]|, p01 = |[ 0 , 1]|, p10 = |[1, 0 ]|, p1 = |[1, 1]|;

      set L1 = { p : (p `1 ) = 0 & (p `2 ) <= 1 & (p `2 ) >= 0 }, L2 = { p : (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 1 }, L3 = { p : (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 0 }, L4 = { p : (p `1 ) = 1 & (p `2 ) <= 1 & (p `2 ) >= 0 };

      

       A1: (p01 `2 ) = 1 by EUCLID: 52;

      

       A2: (p01 `1 ) = 0 by EUCLID: 52;

      

       A3: ( LSeg (p0,p01)) c= L1

      proof

        let a be object;

        assume a in ( LSeg (p0,p01));

        then

        consider lambda such that

         A4: a = (((1 - lambda) * p0) + (lambda * p01)) and

         A5: 0 <= lambda and

         A6: lambda <= 1;

        set q = (((1 - lambda) * p0) + (lambda * p01));

        

         A7: (((1 - lambda) * p0) + (lambda * p01)) = (( 0. ( TOP-REAL 2)) + (lambda * p01)) by EUCLID: 54, RLVECT_1: 10

        .= (lambda * p01) by RLVECT_1: 4

        .= |[(lambda * (p01 `1 )), (lambda * (p01 `2 ))]| by EUCLID: 57

        .= |[ 0 , lambda]| by A2, A1;

        then

         A8: (q `2 ) >= 0 by A5, EUCLID: 52;

        

         A9: (q `1 ) = 0 by A7, EUCLID: 52;

        (q `2 ) <= 1 by A6, A7, EUCLID: 52;

        hence thesis by A4, A9, A8;

      end;

      L1 c= ( LSeg (p0,p01))

      proof

        let a be object;

        assume a in L1;

        then

        consider p such that

         A10: a = p and

         A11: (p `1 ) = 0 and

         A12: (p `2 ) <= 1 and

         A13: (p `2 ) >= 0 ;

        set lambda = (p `2 );

        (((1 - lambda) * p0) + (lambda * p01)) = (( 0. ( TOP-REAL 2)) + (lambda * p01)) by EUCLID: 54, RLVECT_1: 10

        .= (lambda * p01) by RLVECT_1: 4

        .= |[(lambda * (p01 `1 )), (lambda * (p01 `2 ))]| by EUCLID: 57

        .= p by A2, A1, A11, EUCLID: 53;

        hence thesis by A10, A12, A13;

      end;

      hence L1 = ( LSeg (p0,p01)) by A3;

      

       A14: (p1 `2 ) = 1 by EUCLID: 52;

      

       A15: (p1 `1 ) = 1 by EUCLID: 52;

      

       A16: ( LSeg (p01,p1)) c= L2

      proof

        let a be object;

        assume a in ( LSeg (p01,p1));

        then

        consider lambda such that

         A17: a = (((1 - lambda) * p01) + (lambda * p1)) and

         A18: 0 <= lambda and

         A19: lambda <= 1;

        set q = (((1 - lambda) * p01) + (lambda * p1));

        

         A20: (((1 - lambda) * p01) + (lambda * p1)) = ( |[((1 - lambda) * 0 ), ((1 - lambda) * (p01 `2 ))]| + (lambda * p1)) by A2, EUCLID: 57

        .= ( |[ 0 , (1 - lambda)]| + |[lambda, (lambda * 1)]|) by A1, A15, A14, EUCLID: 57

        .= |[( 0 + lambda), ((1 - lambda) + lambda)]| by EUCLID: 56

        .= |[lambda, 1]|;

        then

         A21: (q `1 ) >= 0 by A18, EUCLID: 52;

        

         A22: (q `2 ) = 1 by A20, EUCLID: 52;

        (q `1 ) <= 1 by A19, A20, EUCLID: 52;

        hence thesis by A17, A21, A22;

      end;

      L2 c= ( LSeg (p01,p1))

      proof

        let a be object;

        assume a in L2;

        then

        consider p such that

         A23: a = p and

         A24: (p `1 ) <= 1 and

         A25: (p `1 ) >= 0 and

         A26: (p `2 ) = 1;

        set lambda = (p `1 );

        (((1 - lambda) * p01) + (lambda * p1)) = ( |[((1 - lambda) * 0 ), ((1 - lambda) * (p01 `2 ))]| + (lambda * p1)) by A2, EUCLID: 57

        .= ( |[ 0 , (1 - lambda)]| + |[(lambda * 1), lambda]|) by A1, A15, A14, EUCLID: 57

        .= |[( 0 + lambda), ((1 - lambda) + lambda)]| by EUCLID: 56

        .= p by A26, EUCLID: 53;

        hence thesis by A23, A24, A25;

      end;

      hence L2 = ( LSeg (p01,p1)) by A16;

      

       A27: (p10 `2 ) = 0 by EUCLID: 52;

      

       A28: (p10 `1 ) = 1 by EUCLID: 52;

      

       A29: ( LSeg (p0,p10)) c= L3

      proof

        let a be object;

        assume a in ( LSeg (p0,p10));

        then

        consider lambda such that

         A30: a = (((1 - lambda) * p0) + (lambda * p10)) and

         A31: 0 <= lambda and

         A32: lambda <= 1;

        set q = (((1 - lambda) * p0) + (lambda * p10));

        

         A33: (((1 - lambda) * p0) + (lambda * p10)) = (( 0. ( TOP-REAL 2)) + (lambda * p10)) by EUCLID: 54, RLVECT_1: 10

        .= (lambda * p10) by RLVECT_1: 4

        .= |[(lambda * (p10 `1 )), (lambda * (p10 `2 ))]| by EUCLID: 57

        .= |[lambda, 0 ]| by A28, A27;

        then

         A34: (q `1 ) >= 0 by A31, EUCLID: 52;

        

         A35: (q `2 ) = 0 by A33, EUCLID: 52;

        (q `1 ) <= 1 by A32, A33, EUCLID: 52;

        hence thesis by A30, A34, A35;

      end;

      

       A36: ( LSeg (p10,p1)) c= L4

      proof

        let a be object;

        assume a in ( LSeg (p10,p1));

        then

        consider lambda such that

         A37: a = (((1 - lambda) * p10) + (lambda * p1)) and

         A38: 0 <= lambda and

         A39: lambda <= 1;

        set q = (((1 - lambda) * p10) + (lambda * p1));

        

         A40: (((1 - lambda) * p10) + (lambda * p1)) = ( |[((1 - lambda) * 1), ((1 - lambda) * (p10 `2 ))]| + (lambda * p1)) by A28, EUCLID: 57

        .= ( |[(1 - lambda), 0 ]| + |[lambda, (lambda * 1)]|) by A15, A14, A27, EUCLID: 57

        .= |[((1 - lambda) + lambda), ( 0 + lambda)]| by EUCLID: 56

        .= |[1, lambda]|;

        then

         A41: (q `2 ) >= 0 by A38, EUCLID: 52;

        

         A42: (q `1 ) = 1 by A40, EUCLID: 52;

        (q `2 ) <= 1 by A39, A40, EUCLID: 52;

        hence thesis by A37, A42, A41;

      end;

      L3 c= ( LSeg (p0,p10))

      proof

        let a be object;

        assume a in L3;

        then

        consider p such that

         A43: a = p and

         A44: (p `1 ) <= 1 and

         A45: (p `1 ) >= 0 and

         A46: (p `2 ) = 0 ;

        set lambda = (p `1 );

        (((1 - lambda) * p0) + (lambda * p10)) = (( 0. ( TOP-REAL 2)) + (lambda * p10)) by EUCLID: 54, RLVECT_1: 10

        .= (lambda * p10) by RLVECT_1: 4

        .= |[(lambda * (p10 `1 )), (lambda * (p10 `2 ))]| by EUCLID: 57

        .= p by A28, A27, A46, EUCLID: 53;

        hence thesis by A43, A44, A45;

      end;

      hence L3 = ( LSeg (p0,p10)) by A29;

      L4 c= ( LSeg (p10,p1))

      proof

        let a be object;

        assume a in L4;

        then

        consider p such that

         A47: a = p and

         A48: (p `1 ) = 1 and

         A49: (p `2 ) <= 1 and

         A50: (p `2 ) >= 0 ;

        set lambda = (p `2 );

        (((1 - lambda) * p10) + (lambda * p1)) = ( |[((1 - lambda) * 1), ((1 - lambda) * (p10 `2 ))]| + (lambda * p1)) by A28, EUCLID: 57

        .= ( |[(1 - lambda), 0 ]| + |[(lambda * 1), lambda]|) by A15, A14, A27, EUCLID: 57

        .= |[((1 - lambda) + lambda), ( 0 + lambda)]| by EUCLID: 56

        .= p by A48, EUCLID: 53;

        hence thesis by A47, A49, A50;

      end;

      hence L4 = ( LSeg (p10,p1)) by A36;

    end;

    theorem :: TOPREAL1:14

     R^2-unit_square = { p : (p `1 ) = 0 & (p `2 ) <= 1 & (p `2 ) >= 0 or (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 1 or (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 0 or (p `1 ) = 1 & (p `2 ) <= 1 & (p `2 ) >= 0 }

    proof

      defpred X4[ Point of ( TOP-REAL 2)] means ($1 `1 ) = 1 & ($1 `2 ) <= 1 & ($1 `2 ) >= 0 ;

      defpred X3[ Point of ( TOP-REAL 2)] means ($1 `1 ) <= 1 & ($1 `1 ) >= 0 & ($1 `2 ) = 0 ;

      defpred X2[ Point of ( TOP-REAL 2)] means ($1 `1 ) <= 1 & ($1 `1 ) >= 0 & ($1 `2 ) = 1;

      defpred X1[ Point of ( TOP-REAL 2)] means ($1 `1 ) = 0 & ($1 `2 ) <= 1 & ($1 `2 ) >= 0 ;

      defpred X34[ Point of ( TOP-REAL 2)] means ($1 `1 ) <= 1 & ($1 `1 ) >= 0 & ($1 `2 ) = 0 or ($1 `1 ) = 1 & ($1 `2 ) <= 1 & ($1 `2 ) >= 0 ;

      defpred X12[ Point of ( TOP-REAL 2)] means ($1 `1 ) = 0 & ($1 `2 ) <= 1 & ($1 `2 ) >= 0 or ($1 `1 ) <= 1 & ($1 `1 ) >= 0 & ($1 `2 ) = 1;

      set L1 = { p : X1[p] }, L2 = { p : X2[p] }, L3 = { p : X3[p] }, L4 = { p : X4[p] };

      

       A1: { p2 : X12[p2] or X34[p2] } = ({ p : X12[p] } \/ { q1 : X34[q1] }) from FraenkelAlt;

      

       A2: { q1 : X3[q1] or X4[q1] } = (L3 \/ L4) from FraenkelAlt

      .= (( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) \/ ( LSeg ( |[1, 0 ]|, |[1, 1]|))) by Th13;

      { p : X1[p] or X2[p] } = (L1 \/ L2) from FraenkelAlt

      .= (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) \/ ( LSeg ( |[ 0 , 1]|, |[1, 1]|))) by Th13;

      hence thesis by A1, A2;

    end;

    registration

      cluster R^2-unit_square -> non empty;

      coherence ;

    end

    theorem :: TOPREAL1:15

    (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) /\ ( LSeg ( |[ 0 , 1]|, |[1, 1]|))) = { |[ 0 , 1]|}

    proof

      for a be object holds a in (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) /\ ( LSeg ( |[ 0 , 1]|, |[1, 1]|))) iff a = |[ 0 , 1]|

      proof

        set p00 = |[ 0 , 0 ]|, p01 = |[ 0 , 1]|, p11 = |[1, 1]|;

        let a be object;

        thus a in (( LSeg (p00,p01)) /\ ( LSeg (p01,p11))) implies a = p01

        proof

          assume

           A1: a in (( LSeg (p00,p01)) /\ ( LSeg (p01,p11)));

          then a in { p2 : (p2 `1 ) <= 1 & (p2 `1 ) >= 0 & (p2 `2 ) = 1 } by Th13, XBOOLE_0:def 4;

          then

           A2: ex p2 st p2 = a & (p2 `1 ) <= 1 & (p2 `1 ) >= 0 & (p2 `2 ) = 1;

          a in { p : (p `1 ) = 0 & (p `2 ) <= 1 & (p `2 ) >= 0 } by A1, Th13, XBOOLE_0:def 4;

          then ex p st p = a & (p `1 ) = 0 & (p `2 ) <= 1 & (p `2 ) >= 0 ;

          hence thesis by A2, EUCLID: 53;

        end;

        assume

         A3: a = p01;

        then

         A4: a in ( LSeg (p01,p11)) by RLTOPSP1: 68;

        a in ( LSeg (p00,p01)) by A3, RLTOPSP1: 68;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: TOPREAL1:16

    (( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) /\ ( LSeg ( |[1, 0 ]|, |[1, 1]|))) = { |[1, 0 ]|}

    proof

      for a be object holds a in (( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) /\ ( LSeg ( |[1, 0 ]|, |[1, 1]|))) iff a = |[1, 0 ]|

      proof

        set p00 = |[ 0 , 0 ]|, p10 = |[1, 0 ]|, p11 = |[1, 1]|;

        let a be object;

        thus a in (( LSeg (p00,p10)) /\ ( LSeg (p10,p11))) implies a = p10

        proof

          assume

           A1: a in (( LSeg (p00,p10)) /\ ( LSeg (p10,p11)));

          then a in { p : (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 0 } by Th13, XBOOLE_0:def 4;

          then

           A2: ex p st p = a & (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 0 ;

          a in ( LSeg (p10,p11)) by A1, XBOOLE_0:def 4;

          then ex p2 st p2 = a & (p2 `1 ) = 1 & (p2 `2 ) <= 1 & (p2 `2 ) >= 0 by Th13;

          hence thesis by A2, EUCLID: 53;

        end;

        assume

         A3: a = |[1, 0 ]|;

        then

         A4: a in ( LSeg (p10,p11)) by RLTOPSP1: 68;

        a in ( LSeg (p00,p10)) by A3, RLTOPSP1: 68;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: TOPREAL1:17

    

     Th17: (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) /\ ( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|))) = { |[ 0 , 0 ]|}

    proof

      for a be object holds a in (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) /\ ( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|))) iff a = |[ 0 , 0 ]|

      proof

        let a be object;

        thus a in (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) /\ ( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|))) implies a = |[ 0 , 0 ]|

        proof

          assume

           A1: a in (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) /\ ( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)));

          then a in { p2 : (p2 `1 ) <= 1 & (p2 `1 ) >= 0 & (p2 `2 ) = 0 } by Th13, XBOOLE_0:def 4;

          then

           A2: ex p2 st p2 = a & (p2 `1 ) <= 1 & (p2 `1 ) >= 0 & (p2 `2 ) = 0 ;

          a in ( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) by A1, XBOOLE_0:def 4;

          then ex p st p = a & (p `1 ) = 0 & (p `2 ) <= 1 & (p `2 ) >= 0 by Th13;

          hence thesis by A2, EUCLID: 53;

        end;

        assume

         A3: a = |[ 0 , 0 ]|;

        then

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

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

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: TOPREAL1:18

    

     Th18: (( LSeg ( |[ 0 , 1]|, |[1, 1]|)) /\ ( LSeg ( |[1, 0 ]|, |[1, 1]|))) = { |[1, 1]|}

    proof

      for a be object holds a in (( LSeg ( |[ 0 , 1]|, |[1, 1]|)) /\ ( LSeg ( |[1, 0 ]|, |[1, 1]|))) iff a = |[1, 1]|

      proof

        let a be object;

        thus a in (( LSeg ( |[ 0 , 1]|, |[1, 1]|)) /\ ( LSeg ( |[1, 0 ]|, |[1, 1]|))) implies a = |[1, 1]|

        proof

          assume

           A1: a in (( LSeg ( |[ 0 , 1]|, |[1, 1]|)) /\ ( LSeg ( |[1, 0 ]|, |[1, 1]|)));

          then a in { p : (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 1 } by Th13, XBOOLE_0:def 4;

          then

           A2: ex p st p = a & (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 1;

          a in ( LSeg ( |[1, 0 ]|, |[1, 1]|)) by A1, XBOOLE_0:def 4;

          then ex p2 st p2 = a & (p2 `1 ) = 1 & (p2 `2 ) <= 1 & (p2 `2 ) >= 0 by Th13;

          hence thesis by A2, EUCLID: 53;

        end;

        assume

         A3: a = |[1, 1]|;

        then

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

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

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: TOPREAL1:19

    ( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) misses ( LSeg ( |[ 0 , 1]|, |[1, 1]|))

    proof

      set x = the Element of (( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) /\ ( LSeg ( |[ 0 , 1]|, |[1, 1]|)));

      assume

       A1: (( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) /\ ( LSeg ( |[ 0 , 1]|, |[1, 1]|))) <> {} ;

      then x in ( LSeg ( |[ 0 , 1]|, |[1, 1]|)) by XBOOLE_0:def 4;

      then

       A2: ex p st p = x & (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 1 by Th13;

      x in ( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) by A1, XBOOLE_0:def 4;

      then ex p2 st p2 = x & (p2 `1 ) <= 1 & (p2 `1 ) >= 0 & (p2 `2 ) = 0 by Th13;

      hence contradiction by A2;

    end;

    theorem :: TOPREAL1:20

    

     Th20: ( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) misses ( LSeg ( |[1, 0 ]|, |[1, 1]|))

    proof

      set x = the Element of (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) /\ ( LSeg ( |[1, 0 ]|, |[1, 1]|)));

      assume

       A1: (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) /\ ( LSeg ( |[1, 0 ]|, |[1, 1]|))) <> {} ;

      then x in ( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) by XBOOLE_0:def 4;

      then

       A2: ex p st p = x & (p `1 ) = 0 & (p `2 ) <= 1 & (p `2 ) >= 0 by Th13;

      x in ( LSeg ( |[1, 0 ]|, |[1, 1]|)) by A1, XBOOLE_0:def 4;

      then ex p2 st p2 = x & (p2 `1 ) = 1 & (p2 `2 ) <= 1 & (p2 `2 ) >= 0 by Th13;

      hence contradiction by A2;

    end;

    definition

      let n;

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

      let i;

      :: TOPREAL1:def3

      func LSeg (f,i) -> Subset of ( TOP-REAL n) equals

      : Def3: ( LSeg ((f /. i),(f /. (i + 1)))) if 1 <= i & (i + 1) <= ( len f)

      otherwise {} ;

      coherence

      proof

        thus 1 <= i & (i + 1) <= ( len f) implies ( LSeg ((f /. i),(f /. (i + 1)))) is Subset of ( TOP-REAL n);

        assume i < 1 or ( len f) < (i + 1);

        ( {} ( TOP-REAL n)) is Subset of ( TOP-REAL n);

        hence thesis;

      end;

      correctness ;

    end

    theorem :: TOPREAL1:21

    

     Th21: for f be FinSequence of ( TOP-REAL n) st 1 <= i & (i + 1) <= ( len f) holds (f /. i) in ( LSeg (f,i)) & (f /. (i + 1)) in ( LSeg (f,i))

    proof

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

      assume that

       A1: 1 <= i and

       A2: (i + 1) <= ( len f);

      ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by A1, A2, Def3;

      hence thesis by RLTOPSP1: 68;

    end;

    definition

      let n;

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

      :: TOPREAL1:def4

      func L~ f -> Subset of ( TOP-REAL n) equals ( union { ( LSeg (f,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f) });

      coherence

      proof

        set F = { ( LSeg (f,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f) };

        F c= ( bool the carrier of ( TOP-REAL n))

        proof

          let a be object;

          assume a in F;

          then ex i be Nat st a = ( LSeg (f,i)) & 1 <= i & (i + 1) <= ( len f);

          hence thesis;

        end;

        then

        reconsider F as Subset-Family of ( TOP-REAL n);

        ( union F) is Subset of ( TOP-REAL n);

        hence thesis;

      end;

    end

    theorem :: TOPREAL1:22

    

     Th22: for f be FinSequence of ( TOP-REAL n) holds ( len f) = 0 or ( len f) = 1 iff ( L~ f) = {}

    proof

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

      thus (( len f) = 0 or ( len f) = 1) implies ( L~ f) = {}

      proof

        set L = { ( LSeg (f,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f) };

        set x = the Element of L;

        assume

         A1: ( len f) = 0 or ( len f) = 1;

        now

          per cases by A1;

            suppose

             A2: ( len f) = 0 ;

            now

              assume L <> {} ;

              then x in L;

              then ex i be Nat st x = ( LSeg (f,i)) & 1 <= i & (i + 1) <= ( len f);

              hence contradiction by A2;

            end;

            hence thesis by ZFMISC_1: 2;

          end;

            suppose

             A3: ( len f) = ( 0 + 1);

            now

              assume L <> {} ;

              then x in L;

              then ex i be Nat st x = ( LSeg (f,i)) & 1 <= i & (i + 1) <= ( len f);

              hence contradiction by A3, XREAL_1: 6;

            end;

            hence thesis by ZFMISC_1: 2;

          end;

        end;

        hence thesis;

      end;

      set L = { ( LSeg (f,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f) };

      assume

       A4: ( L~ f) = {} ;

      assume that

       A5: ( len f) <> 0 and

       A6: ( len f) <> 1;

      now

        assume ( len f) <= 1;

        then ( len f) < ( 0 + 1) by A6, XXREAL_0: 1;

        hence contradiction by A5, NAT_1: 13;

      end;

      then

       A7: ( len f) >= (1 + 1) by NAT_1: 13;

      then ( LSeg (f,1)) in L;

      then ( LSeg (f,1)) = {} by A4, XBOOLE_1: 3, ZFMISC_1: 74;

      hence contradiction by A7, Th21;

    end;

    theorem :: TOPREAL1:23

    

     Th23: for f be FinSequence of ( TOP-REAL n) holds ( len f) >= 2 implies ( L~ f) <> {}

    proof

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

      assume

       A1: ( len f) >= 2;

      then not ( len f) = 1;

      hence thesis by A1, Th22;

    end;

    definition

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

      :: TOPREAL1:def5

      attr IT is special means for i st 1 <= i & (i + 1) <= ( len IT) holds ((IT /. i) `1 ) = ((IT /. (i + 1)) `1 ) or ((IT /. i) `2 ) = ((IT /. (i + 1)) `2 );

      :: TOPREAL1:def6

      attr IT is unfolded means for i st 1 <= i & (i + 2) <= ( len IT) holds (( LSeg (IT,i)) /\ ( LSeg (IT,(i + 1)))) = {(IT /. (i + 1))};

      :: TOPREAL1:def7

      attr IT is s.n.c. means for i, j st (i + 1) < j holds ( LSeg (IT,i)) misses ( LSeg (IT,j));

    end

    reserve f,f1,f2,h for FinSequence of ( TOP-REAL 2);

    definition

      let f;

      :: TOPREAL1:def8

      attr f is being_S-Seq means f is one-to-one & ( len f) >= 2 & f is unfolded s.n.c. special;

    end

    theorem :: TOPREAL1:24

    

     Th24: ex f1, f2 st f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (( L~ f1) \/ ( L~ f2)) & (( L~ f1) /\ ( L~ f2)) = { |[ 0 , 0 ]|, |[1, 1]|} & (f1 /. 1) = |[ 0 , 0 ]| & (f1 /. ( len f1)) = |[1, 1]| & (f2 /. 1) = |[ 0 , 0 ]| & (f2 /. ( len f2)) = |[1, 1]|

    proof

      set p0 = |[ 0 , 0 ]|, p01 = |[ 0 , 1]|, p10 = |[1, 0 ]|, p1 = |[1, 1]|;

      set L4 = { p : (p `1 ) = 1 & (p `2 ) <= 1 & (p `2 ) >= 0 };

      set L3 = { p : (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 0 };

      set L2 = { p : (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 1 };

      set L1 = { p : (p `1 ) = 0 & (p `2 ) <= 1 & (p `2 ) >= 0 };

      

       A1: (p1 `1 ) = 1 by EUCLID: 52;

      reconsider f2 = <*p0, p10, p1*> as FinSequence of ( TOP-REAL 2);

      reconsider f1 = <*p0, p01, p1*> as FinSequence of ( TOP-REAL 2);

      

       A2: (p0 `1 ) = 0 by EUCLID: 52;

      take f1, f2;

      

       A3: (f1 /. 2) = p01 by FINSEQ_4: 18;

      now

        assume L2 meets L3;

        then

        consider x be object such that

         A4: x in L2 and

         A5: x in L3 by XBOOLE_0: 3;

        

         A6: ex p2 st p2 = x & (p2 `1 ) <= 1 & (p2 `1 ) >= 0 & (p2 `2 ) = 0 by A5;

        ex p st p = x & (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 1 by A4;

        hence contradiction by A6;

      end;

      then

       A7: (L2 /\ L3) = {} ;

      

       A8: (p10 `2 ) = 0 by EUCLID: 52;

      

       A9: (p10 `1 ) = 1 by EUCLID: 52;

      

       A10: ( len f2) = (1 + 2) by FINSEQ_1: 45;

      then

       A11: (1 + 1) <= ( len f2);

      

       A12: (f1 /. 3) = p1 by FINSEQ_4: 18;

      

       A13: (f1 /. 1) = p0 by FINSEQ_4: 18;

      

       A14: { ( LSeg (f1,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f1) } c= {( LSeg (p0,p01)), ( LSeg (p01,p1))}

      proof

        let a be object;

        assume a in { ( LSeg (f1,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f1) };

        then

        consider i be Nat such that

         A15: a = ( LSeg (f1,i)) and

         A16: 1 <= i and

         A17: (i + 1) <= ( len f1);

        (i + 1) <= (2 + 1) by A17, FINSEQ_1: 45;

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

        then i = 1 or i = 2 by A16, NAT_1: 9;

        then a = ( LSeg (p0,p01)) or a = ( LSeg (p01,p1)) by A13, A3, A12, A15, A17, Def3;

        hence thesis by TARSKI:def 2;

      end;

      

       A18: ( len f1) = (1 + 2) by FINSEQ_1: 45;

      then

       A19: (1 + 1) <= ( len f1);

      (1 + 1) in ( Seg ( len f1)) by A18, FINSEQ_1: 1;

      then ( LSeg (p0,p01)) = ( LSeg (f1,1)) by A18, A13, A3, Def3;

      then

       A20: ( LSeg (p0,p01)) in { ( LSeg (f1,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f1) } by A19;

      

       A21: (f2 /. 3) = p1 by FINSEQ_4: 18;

      

       A22: (p0 `2 ) = 0 by EUCLID: 52;

      thus f1 is being_S-Seq

      proof

        

         A23: p01 <> p1 by A1, EUCLID: 52;

        p0 <> p01 by A22, EUCLID: 52;

        hence f1 is one-to-one by A1, A2, A23, FINSEQ_3: 95;

        thus ( len f1) >= 2 by A18;

        thus f1 is unfolded

        proof

          

           A24: for x be object holds x in (( LSeg (p0,p01)) /\ ( LSeg (p01,p1))) iff x = p01

          proof

            let x be object;

            thus x in (( LSeg (p0,p01)) /\ ( LSeg (p01,p1))) implies x = p01

            proof

              assume

               A25: x in (( LSeg (p0,p01)) /\ ( LSeg (p01,p1)));

              then x in { p2 : (p2 `1 ) <= 1 & (p2 `1 ) >= 0 & (p2 `2 ) = 1 } by Th13, XBOOLE_0:def 4;

              then

               A26: ex p2 st p2 = x & (p2 `1 ) <= 1 & (p2 `1 ) >= 0 & (p2 `2 ) = 1;

              x in { p : (p `1 ) = 0 & (p `2 ) <= 1 & (p `2 ) >= 0 } by A25, Th13, XBOOLE_0:def 4;

              then ex p st p = x & (p `1 ) = 0 & (p `2 ) <= 1 & (p `2 ) >= 0 ;

              hence thesis by A26, EUCLID: 53;

            end;

            assume

             A27: x = p01;

            then

             A28: x in ( LSeg (p01,p1)) by RLTOPSP1: 68;

            x in ( LSeg (p0,p01)) by A27, RLTOPSP1: 68;

            hence thesis by A28, XBOOLE_0:def 4;

          end;

          let i;

          assume that

           A29: 1 <= i and

           A30: (i + 2) <= ( len f1);

          i <= 1 by A18, A30, XREAL_1: 6;

          then

           A31: i = 1 by A29, XXREAL_0: 1;

          (1 + 1) in ( Seg ( len f1)) by A18, FINSEQ_1: 1;

          then

           A32: ( LSeg (f1,1)) = ( LSeg (p0,p01)) by A18, A13, A3, Def3;

          ( LSeg (f1,(1 + 1))) = ( LSeg (p01,p1)) by A18, A3, A12, Def3;

          hence thesis by A3, A31, A32, A24, TARSKI:def 1;

        end;

        thus f1 is s.n.c.

        proof

          let i, j such that

           A33: (i + 1) < j;

          now

            per cases ;

              suppose 1 <= i;

              then

               A34: (1 + 1) <= (i + 1) by XREAL_1: 6;

              now

                per cases ;

                  case 1 <= j & (j + 1) <= ( len f1);

                  then j <= 2 by A18, XREAL_1: 6;

                  hence contradiction by A33, A34, XXREAL_0: 2;

                end;

                  case not (1 <= j & (j + 1) <= ( len f1));

                  then ( LSeg (f1,j)) = {} by Def3;

                  hence (( LSeg (f1,i)) /\ ( LSeg (f1,j))) = {} ;

                end;

              end;

              hence (( LSeg (f1,i)) /\ ( LSeg (f1,j))) = {} ;

            end;

              suppose not (1 <= i & (i + 1) <= ( len f1));

              then ( LSeg (f1,i)) = {} by Def3;

              hence (( LSeg (f1,i)) /\ ( LSeg (f1,j))) = {} ;

            end;

          end;

          hence (( LSeg (f1,i)) /\ ( LSeg (f1,j))) = {} ;

        end;

        let i;

        assume that

         A35: 1 <= i and

         A36: (i + 1) <= ( len f1);

        

         A37: i <= (1 + 1) by A18, A36, XREAL_1: 6;

        per cases by A35, A37, NAT_1: 9;

          suppose

           A38: i = 1;

          

          then ((f1 /. i) `1 ) = (p0 `1 ) by FINSEQ_4: 18

          .= 0 by EUCLID: 52

          .= ((f1 /. (i + 1)) `1 ) by A3, A38, EUCLID: 52;

          hence thesis;

        end;

          suppose

           A39: i = 2;

          

          then ((f1 /. i) `2 ) = (p01 `2 ) by FINSEQ_4: 18

          .= 1 by EUCLID: 52

          .= ((f1 /. (i + 1)) `2 ) by A12, A39, EUCLID: 52;

          hence thesis;

        end;

      end;

      

       A40: (f2 /. 2) = p10 by FINSEQ_4: 18;

      

       A41: (f2 /. 1) = p0 by FINSEQ_4: 18;

      

       A42: { ( LSeg (f2,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f2) } c= {( LSeg (p0,p10)), ( LSeg (p10,p1))}

      proof

        let a be object;

        assume a in { ( LSeg (f2,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f2) };

        then

        consider i be Nat such that

         A43: a = ( LSeg (f2,i)) and

         A44: 1 <= i and

         A45: (i + 1) <= ( len f2);

        (i + 1) <= (2 + 1) by A45, FINSEQ_1: 45;

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

        then i = 1 or i = 2 by A44, NAT_1: 9;

        then a = ( LSeg (p0,p10)) or a = ( LSeg (p10,p1)) by A41, A40, A21, A43, A45, Def3;

        hence thesis by TARSKI:def 2;

      end;

      (1 + 1) in ( Seg ( len f2)) by A10, FINSEQ_1: 1;

      then ( LSeg (p0,p10)) = ( LSeg (f2,1)) by A10, A41, A40, Def3;

      then

       A46: ( LSeg (p0,p10)) in { ( LSeg (f2,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f2) } by A11;

      ( LSeg (p10,p1)) = ( LSeg (f2,2)) by A10, A40, A21, Def3;

      then ( LSeg (p10,p1)) in { ( LSeg (f2,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f2) } by A10;

      then {( LSeg (p0,p10)), ( LSeg (p10,p1))} c= { ( LSeg (f2,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f2) } by A46, ZFMISC_1: 32;

      then

       A47: ( L~ f2) = ( union {( LSeg (p0,p10)), ( LSeg (p10,p1))}) by A42, XBOOLE_0:def 10;

      

       A48: (p1 `2 ) = 1 by EUCLID: 52;

      thus f2 is being_S-Seq

      proof

        thus f2 is one-to-one by A1, A48, A9, A8, A2, FINSEQ_3: 95;

        thus ( len f2) >= 2 by A10;

        thus f2 is unfolded

        proof

          

           A49: for x be object holds x in (( LSeg (p0,p10)) /\ ( LSeg (p10,p1))) iff x = p10

          proof

            let x be object;

            thus x in (( LSeg (p0,p10)) /\ ( LSeg (p10,p1))) implies x = p10

            proof

              assume

               A50: x in (( LSeg (p0,p10)) /\ ( LSeg (p10,p1)));

              then x in { p2 : (p2 `1 ) = 1 & (p2 `2 ) <= 1 & (p2 `2 ) >= 0 } by Th13, XBOOLE_0:def 4;

              then

               A51: ex p2 st p2 = x & (p2 `1 ) = 1 & (p2 `2 ) <= 1 & (p2 `2 ) >= 0 ;

              x in { p : (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 0 } by A50, Th13, XBOOLE_0:def 4;

              then ex p st p = x & (p `1 ) <= 1 & (p `1 ) >= 0 & (p `2 ) = 0 ;

              hence thesis by A51, EUCLID: 53;

            end;

            assume

             A52: x = p10;

            then

             A53: x in ( LSeg (p10,p1)) by RLTOPSP1: 68;

            x in ( LSeg (p0,p10)) by A52, RLTOPSP1: 68;

            hence thesis by A53, XBOOLE_0:def 4;

          end;

          let i;

          assume that

           A54: 1 <= i and

           A55: (i + 2) <= ( len f2);

          i <= 1 by A10, A55, XREAL_1: 6;

          then

           A56: i = 1 by A54, XXREAL_0: 1;

          (1 + 1) in ( Seg ( len f2)) by A10, FINSEQ_1: 1;

          then

           A57: ( LSeg (f2,1)) = ( LSeg (p0,p10)) by A10, A41, A40, Def3;

          ( LSeg (f2,(1 + 1))) = ( LSeg (p10,p1)) by A10, A40, A21, Def3;

          hence thesis by A40, A56, A57, A49, TARSKI:def 1;

        end;

        thus f2 is s.n.c.

        proof

          let i, j such that

           A58: (i + 1) < j;

          per cases ;

            suppose 1 <= i;

            then

             A59: (1 + 1) <= (i + 1) by XREAL_1: 6;

            now

              per cases ;

                case 1 <= j & (j + 1) <= ( len f2);

                then j <= 2 by A10, XREAL_1: 6;

                hence contradiction by A58, A59, XXREAL_0: 2;

              end;

                case not (1 <= j & (j + 1) <= ( len f2));

                then ( LSeg (f2,j)) = {} by Def3;

                hence (( LSeg (f2,i)) /\ ( LSeg (f2,j))) = {} ;

              end;

            end;

            hence (( LSeg (f2,i)) /\ ( LSeg (f2,j))) = {} ;

          end;

            suppose not (1 <= i & (i + 1) <= ( len f2));

            then ( LSeg (f2,i)) = {} by Def3;

            hence (( LSeg (f2,i)) /\ ( LSeg (f2,j))) = {} ;

          end;

        end;

        let i;

        assume that

         A60: 1 <= i and

         A61: (i + 1) <= ( len f2);

        

         A62: i <= (1 + 1) by A10, A61, XREAL_1: 6;

        per cases by A60, A62, NAT_1: 9;

          suppose

           A63: i = 1;

          

          then ((f2 /. i) `2 ) = (p0 `2 ) by FINSEQ_4: 18

          .= 0 by EUCLID: 52

          .= ((f2 /. (i + 1)) `2 ) by A40, A63, EUCLID: 52;

          hence thesis;

        end;

          suppose

           A64: i = 2;

          

          then ((f2 /. i) `1 ) = (p10 `1 ) by FINSEQ_4: 18

          .= 1 by EUCLID: 52

          .= ((f2 /. (i + 1)) `1 ) by A21, A64, EUCLID: 52;

          hence thesis;

        end;

      end;

      

       A65: (( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) /\ ( LSeg ( |[1, 0 ]|, |[1, 1]|))) = {} by Th20;

      ( LSeg (p01,p1)) = ( LSeg (f1,2)) by A18, A3, A12, Def3;

      then ( LSeg (p01,p1)) in { ( LSeg (f1,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f1) } by A18;

      then {( LSeg (p0,p01)), ( LSeg (p01,p1))} c= { ( LSeg (f1,i)) where i be Nat : 1 <= i & (i + 1) <= ( len f1) } by A20, ZFMISC_1: 32;

      then

       A66: ( L~ f1) = ( union {( LSeg (p0,p01)), ( LSeg (p01,p1))}) by A14, XBOOLE_0:def 10;

      then ( L~ f1) = (( LSeg (p0,p01)) \/ ( LSeg (p01,p1))) by ZFMISC_1: 75;

      hence R^2-unit_square = (( L~ f1) \/ ( L~ f2)) by A47, ZFMISC_1: 75;

      ( L~ f2) = (( LSeg (p0,p10)) \/ ( LSeg (p10,p1))) by A47, ZFMISC_1: 75;

      

      hence (( L~ f1) /\ ( L~ f2)) = ((L1 \/ L2) /\ (L3 \/ L4)) by A66, Th13, ZFMISC_1: 75

      .= (((L1 \/ L2) /\ L3) \/ ((L1 \/ L2) /\ L4)) by XBOOLE_1: 23

      .= (((L1 /\ L3) \/ (L2 /\ L3)) \/ ((L1 \/ L2) /\ L4)) by XBOOLE_1: 23

      .= (((L1 /\ L3) \/ (L2 /\ L3)) \/ ((L1 /\ L4) \/ (L2 /\ L4))) by XBOOLE_1: 23

      .= { |[ 0 , 0 ]|, |[1, 1]|} by A7, A65, Th13, Th17, Th18, ENUMSET1: 1;

      thus thesis by A18, A10, FINSEQ_4: 18;

    end;

    theorem :: TOPREAL1:25

    

     Th25: h is being_S-Seq implies ( L~ h) is_an_arc_of ((h /. 1),(h /. ( len h)))

    proof

      set P = ( L~ h);

      set p1 = (h /. 1);

      deffunc Q( Nat) = ( L~ (h | ($1 + 2)));

      defpred ARC[ Nat] means 1 <= ($1 + 2) & ($1 + 2) <= ( len h) implies ex NE be non empty Subset of ( TOP-REAL 2) st NE = Q($1) & ex f be Function of I[01] , (( TOP-REAL 2) | NE) st f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = (h /. ($1 + 2));

      set p2 = (h /. (1 + 1));

      assume

       A1: h is being_S-Seq;

      then

       A2: ( len h) >= (1 + 1);

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

      then

       A3: 1 in ( Seg ( len h)) by FINSEQ_1: 1;

      

       A4: h is one-to-one by A1;

      

       A5: for n st ARC[n] holds ARC[(n + 1)]

      proof

        let n;

        assume

         A6: ARC[n];

        set pn = (h /. (n + 2)), pn1 = (h /. ((n + 2) + 1));

        

         A7: ((n + 1) + 1) <> ((n + 2) + 1);

        reconsider NE1 = ( Q(n) \/ ( LSeg (pn,pn1))) as non empty Subset of ( TOP-REAL 2);

        assume that

         A8: 1 <= ((n + 1) + 2) and

         A9: ((n + 1) + 2) <= ( len h);

        

         A10: ((n + 2) + 1) in ( dom h) by A8, A9, FINSEQ_3: 25;

        

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

        then

        consider NE be non empty Subset of ( TOP-REAL 2) such that

         A12: NE = Q(n) and

         A13: ex f be Function of I[01] , (( TOP-REAL 2) | NE) st f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = (h /. (n + 2)) by A6, A9, NAT_1: 11, XXREAL_0: 2;

        

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

        now

          let x be object such that

           A15: x in ( Q(n) \/ ( LSeg (h,(n + 2))));

          now

            per cases by A15, XBOOLE_0:def 3;

              suppose

               A16: x in Q(n);

              

               A17: (n + 1) <= (n + (1 + 1)) by XREAL_1: 6;

              consider X be set such that

               A18: x in X and

               A19: X in { ( LSeg ((h | (n + 2)),i)) where i be Nat : 1 <= i & (i + 1) <= ( len (h | (n + 2))) } by A16, TARSKI:def 4;

              consider i be Nat such that

               A20: X = ( LSeg ((h | (n + 2)),i)) and

               A21: 1 <= i and

               A22: (i + 1) <= ( len (h | (n + 2))) by A19;

              (i + 1) <= ((n + 1) + 1) by A9, A11, A22, FINSEQ_1: 59, XXREAL_0: 2;

              then i <= (n + 1) by XREAL_1: 6;

              then

               A23: i <= (n + 2) by A17, XXREAL_0: 2;

              ( len (h | (n + 2))) = (n + 2) by A9, A11, FINSEQ_1: 59, XXREAL_0: 2;

              then i in ( Seg ( len (h | (n + 2)))) by A21, A23, FINSEQ_1: 1;

              then

               A24: i in ( dom (h | (n + 2))) by FINSEQ_1:def 3;

              set p19 = ((h | (n + 2)) /. i), p29 = ((h | (n + 2)) /. (i + 1));

              

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

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

              then i in ( Seg ((n + 1) + 2)) by A21, FINSEQ_1: 1;

              then i in ( Seg ( len (h | ((n + 1) + 2)))) by A9, FINSEQ_1: 59;

              then i in ( dom (h | ((n + 1) + 2))) by FINSEQ_1:def 3;

              

              then

               A26: ((h | ((n + 1) + 2)) /. i) = (h /. i) by FINSEQ_4: 70

              .= p19 by A24, FINSEQ_4: 70;

              (i + 1) <= (n + 2) by A9, A11, A22, FINSEQ_1: 59, XXREAL_0: 2;

              then

               A27: (i + 1) <= ((n + 1) + 2) by A25, XXREAL_0: 2;

              

               A28: ( len (h | ((n + 1) + 2))) = ((n + 1) + 2) by A9, FINSEQ_1: 59;

              

               A29: ( len (h | ((n + 1) + 2))) = (n + (1 + 2)) by A9, FINSEQ_1: 59;

              

               A30: (n + 2) <= (n + 3) by XREAL_1: 6;

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

              then (i + 1) in ( Seg ( len (h | (n + 2)))) by A22, FINSEQ_1: 1;

              then

               A31: (i + 1) in ( dom (h | (n + 2))) by FINSEQ_1:def 3;

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

              then (i + 1) in ( Seg ((n + 1) + 2)) by A27, FINSEQ_1: 1;

              then (i + 1) in ( Seg ( len (h | ((n + 1) + 2)))) by A9, FINSEQ_1: 59;

              then (i + 1) in ( dom (h | ((n + 1) + 2))) by FINSEQ_1:def 3;

              

              then

               A32: ((h | ((n + 1) + 2)) /. (i + 1)) = (h /. (i + 1)) by FINSEQ_4: 70

              .= p29 by A31, FINSEQ_4: 70;

              (i + 1) <= (n + (1 + 1)) by A9, A11, A22, FINSEQ_1: 59, XXREAL_0: 2;

              then

               A33: (i + 1) <= ( len (h | ((n + 1) + 2))) by A29, A30, XXREAL_0: 2;

              X = ( LSeg (p19,p29)) by A20, A21, A22, Def3

              .= ( LSeg ((h | ((n + 1) + 2)),i)) by A21, A27, A28, A26, A32, Def3;

              then X in { ( LSeg ((h | ((n + 1) + 2)),j)) where j be Nat : 1 <= j & (j + 1) <= ( len (h | ((n + 1) + 2))) } by A21, A33;

              hence x in Q(+) by A18, TARSKI:def 4;

            end;

              suppose

               A34: x in ( LSeg (h,(n + 2)));

              

               A35: 1 <= (n + 2) by A14, NAT_1: 11;

              

               A36: ( len (h | ((n + 1) + 2))) = ((n + 1) + 2) by A9, FINSEQ_1: 59;

              then ((n + 2) + 1) in ( Seg ( len (h | ((n + 1) + 2)))) by A8, FINSEQ_1: 1;

              then

               A37: ((n + 2) + 1) in ( dom (h | ((n + 1) + 2))) by FINSEQ_1:def 3;

              then

               A38: ((n + 2) + 1) <= ( len (h | ((n + 1) + 2))) by FINSEQ_3: 25;

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

              then (n + 2) in ( Seg ( len (h | ((n + 1) + 2)))) by A36, A35, FINSEQ_1: 1;

              then

               A39: (n + 2) in ( dom (h | ((n + 1) + 2))) by FINSEQ_1:def 3;

              then

               A40: 1 <= (n + 2) by FINSEQ_3: 25;

              

               A41: pn1 = ((h | ((n + 1) + 2)) /. ((n + 2) + 1)) by A37, FINSEQ_4: 70;

              

               A42: pn = ((h | ((n + 1) + 2)) /. (n + 2)) by A39, FINSEQ_4: 70;

              ( LSeg (h,(n + 2))) = ( LSeg (pn,pn1)) by A9, A35, Def3

              .= ( LSeg ((h | ((n + 1) + 2)),(n + 2))) by A36, A35, A42, A41, Def3;

              then ( LSeg (h,(n + 2))) in { ( LSeg ((h | ((n + 1) + 2)),i)) where i be Nat : 1 <= i & (i + 1) <= ( len (h | ((n + 1) + 2))) } by A40, A38;

              hence x in Q(+) by A34, TARSKI:def 4;

            end;

          end;

          hence x in Q(+);

        end;

        then

         A43: ( Q(n) \/ ( LSeg (h,(n + 2)))) c= Q(+);

        take NE1;

        

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

        now

          let x be object;

          

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

          

           A46: (( len (h | ((n + 1) + 2))) - 1) = (((n + 1) + 2) - 1) by A9, FINSEQ_1: 59

          .= (n + (1 + 1));

          assume x in Q(+);

          then

          consider X be set such that

           A47: x in X and

           A48: X in { ( LSeg ((h | ((n + 1) + 2)),i)) where i be Nat : 1 <= i & (i + 1) <= ( len (h | ((n + 1) + 2))) } by TARSKI:def 4;

          consider i be Nat such that

           A49: X = ( LSeg ((h | ((n + 1) + 2)),i)) and

           A50: 1 <= i and

           A51: (i + 1) <= ( len (h | ((n + 1) + 2))) by A48;

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

          then

           A52: i <= (( len (h | ((n + 1) + 2))) - 1) by A51, XREAL_1: 9;

          now

            per cases by A52, A46, A45, NAT_1: 8;

              suppose

               A53: i = (n + 2);

              

               A54: ( len (h | ((n + 1) + 2))) = ((n + 1) + 2) by A9, FINSEQ_1: 59;

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

              then ((n + 2) + 1) in ( Seg ( len (h | ((n + 1) + 2)))) by A54, FINSEQ_1: 1;

              then ((n + 2) + 1) in ( dom (h | ((n + 1) + 2))) by FINSEQ_1:def 3;

              then

               A55: ((h | ((n + 1) + 2)) /. ((n + 2) + 1)) = (h /. (n + (2 + 1))) by FINSEQ_4: 70;

              

               A56: 1 <= (n + 2) by A14, NAT_1: 11;

              ((n + 1) + 2) = ((n + 2) + 1);

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

              then (n + 2) in ( Seg ( len (h | ((n + 1) + 2)))) by A54, A56, FINSEQ_1: 1;

              then (n + 2) in ( dom (h | ((n + 1) + 2))) by FINSEQ_1:def 3;

              then ((h | ((n + 1) + 2)) /. (n + 2)) = (h /. (n + 2)) by FINSEQ_4: 70;

              

              then ( LSeg ((h | ((n + 1) + 2)),(n + 2))) = ( LSeg (pn,pn1)) by A54, A56, A55, Def3

              .= ( LSeg (h,(n + 2))) by A9, A44, Def3;

              hence x in ( Q(n) \/ ( LSeg (h,(n + 2)))) by A47, A49, A53, XBOOLE_0:def 3;

            end;

              suppose

               A57: i <= (n + 1);

              then (i + 1) <= ((n + 1) + 1) by XREAL_1: 6;

              then (i + 1) <= ( len (h | (n + 2))) by A9, A11, FINSEQ_1: 59, XXREAL_0: 2;

              then

               A58: ( LSeg ((h | (n + 2)),i)) in { ( LSeg ((h | (n + 2)),j)) where j be Nat : 1 <= j & (j + 1) <= ( len (h | (n + 2))) } by A50;

              set p19 = ((h | (n + 2)) /. i), p29 = ((h | (n + 2)) /. (i + 1));

              

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

              

               A60: ( len (h | (n + 2))) = (n + (1 + 1)) by A9, A11, FINSEQ_1: 59, XXREAL_0: 2;

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

              then

               A61: i <= (n + 2) by A57, XXREAL_0: 2;

              then i in ( Seg ( len (h | (n + 2)))) by A50, A60, FINSEQ_1: 1;

              then

               A62: i in ( dom (h | (n + 2))) by FINSEQ_1:def 3;

              

               A63: (i + 1) <= ((n + 1) + 1) by A57, XREAL_1: 7;

              then (i + 1) in ( Seg ( len (h | (n + 2)))) by A60, A59, FINSEQ_1: 1;

              then

               A64: (i + 1) in ( dom (h | (n + 2))) by FINSEQ_1:def 3;

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

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

              then i in ( Seg ((n + 1) + 2)) by A50, FINSEQ_1: 1;

              then i in ( Seg ( len (h | ((n + 1) + 2)))) by A9, FINSEQ_1: 59;

              then i in ( dom (h | ((n + 1) + 2))) by FINSEQ_1:def 3;

              

              then

               A65: ((h | ((n + 1) + 2)) /. i) = (h /. i) by FINSEQ_4: 70

              .= p19 by A62, FINSEQ_4: 70;

              (i + 1) <= ((n + 1) + 2) by A57, XREAL_1: 7;

              then (i + 1) in ( Seg ((n + 1) + 2)) by A59, FINSEQ_1: 1;

              then (i + 1) in ( Seg ( len (h | ((n + 1) + 2)))) by A9, FINSEQ_1: 59;

              then (i + 1) in ( dom (h | ((n + 1) + 2))) by FINSEQ_1:def 3;

              

              then

               A66: ((h | ((n + 1) + 2)) /. (i + 1)) = (h /. (i + 1)) by FINSEQ_4: 70

              .= p29 by A64, FINSEQ_4: 70;

              ( LSeg ((h | (n + 2)),i)) = ( LSeg (p19,p29)) by A50, A60, A63, Def3

              .= ( LSeg ((h | ((n + 1) + 2)),i)) by A50, A51, A65, A66, Def3;

              then x in ( union { ( LSeg ((h | (n + 2)),j)) where j be Nat : 1 <= j & (j + 1) <= ( len (h | (n + 2))) }) by A47, A49, A58, TARSKI:def 4;

              hence x in ( Q(n) \/ ( LSeg (h,(n + 2)))) by XBOOLE_0:def 3;

            end;

          end;

          hence x in ( Q(n) \/ ( LSeg (h,(n + 2))));

        end;

        then Q(+) c= ( Q(n) \/ ( LSeg (h,(n + 2))));

        then Q(+) = ( Q(n) \/ ( LSeg (h,(n + 2)))) by A43;

        hence NE1 = Q(+) by A9, A44, Def3;

        

         A67: ((n + 1) + 1) <= ( len h) by A9, A11, XXREAL_0: 2;

        then ((n + 1) + 1) in ( dom h) by A44, FINSEQ_3: 25;

        then ( LSeg (pn,pn1)) is_an_arc_of (pn,pn1) by A4, A7, A10, Th9, PARTFUN2: 10;

        then

        consider f1 be Function of I[01] , (( TOP-REAL 2) | ( LSeg (pn,pn1))) such that

         A68: f1 is being_homeomorphism and

         A69: (f1 . 0 ) = pn and

         A70: (f1 . 1) = pn1;

        consider f be Function of I[01] , (( TOP-REAL 2) | NE) such that f is being_homeomorphism and

         A71: (f . 0 ) = p1 and (f . 1) = (h /. (n + 2)) by A13;

        for x be object holds x in ( Q(n) /\ ( LSeg (pn,pn1))) iff x = pn

        proof

          let x be object;

          

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

          thus x in ( Q(n) /\ ( LSeg (pn,pn1))) implies x = pn

          proof

            

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

            h is unfolded by A1;

            then

             A74: (( LSeg (h,(n + 1))) /\ ( LSeg (h,((n + 1) + 1)))) = {(h /. ((n + 1) + 1))} by A9, A73;

            

             A75: ((n + 1) + 1) <= ( len h) by A9, A11, XXREAL_0: 2;

            assume

             A76: x in ( Q(n) /\ ( LSeg (pn,pn1)));

            then

             A77: x in ( LSeg (pn,pn1)) by XBOOLE_0:def 4;

            

             A78: ( LSeg (pn,pn1)) = ( LSeg (h,((n + 1) + 1))) by A9, A44, Def3;

            set p19 = (h /. (n + 1)), p29 = (h /. ((n + 1) + 1));

            

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

            x in Q(n) by A76, XBOOLE_0:def 4;

            then

            consider X be set such that

             A80: x in X and

             A81: X in { ( LSeg ((h | (n + 2)),i)) where i be Nat : 1 <= i & (i + 1) <= ( len (h | (n + 2))) } by TARSKI:def 4;

            consider i be Nat such that

             A82: X = ( LSeg ((h | (n + 2)),i)) and

             A83: 1 <= i and

             A84: (i + 1) <= ( len (h | (n + 2))) by A81;

            

             A85: ( len (h | (n + 2))) = (n + (1 + 1)) by A9, A11, FINSEQ_1: 59, XXREAL_0: 2;

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

            then (n + 1) in ( Seg ( len (h | (n + 2)))) by A85, A79, FINSEQ_1: 1;

            then (n + 1) in ( dom (h | (n + 2))) by FINSEQ_1:def 3;

            then

             A86: ((h | (n + 2)) /. (n + 1)) = p19 by FINSEQ_4: 70;

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

            then ((n + 1) + 1) in ( Seg ( len (h | (n + 2)))) by A85, FINSEQ_1: 1;

            then ((n + 1) + 1) in ( dom (h | (n + 2))) by FINSEQ_1:def 3;

            then

             A87: ((h | (n + 2)) /. ((n + 1) + 1)) = p29 by FINSEQ_4: 70;

            

             A88: ( len (h | (n + 2))) = ((n + 1) + 1) by A9, A11, FINSEQ_1: 59, XXREAL_0: 2;

            then

             A89: i <= (n + 1) by A84, XREAL_1: 6;

            then 1 <= (n + 1) by A83, XXREAL_0: 2;

            

            then

             A90: ( LSeg (h,(n + 1))) = ( LSeg (p19,p29)) by A75, Def3

            .= ( LSeg ((h | (n + 2)),(n + 1))) by A85, A79, A86, A87, Def3;

            

             A91: h is s.n.c. by A1;

            now

              set p19 = (h /. i), p29 = (h /. (i + 1));

              assume

               A92: i < (n + 1);

              then

               A93: (i + 1) < ((n + 1) + 1) by XREAL_1: 6;

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

              then i <= (n + 2) by A92, XXREAL_0: 2;

              then i in ( Seg ( len (h | (n + 2)))) by A83, A85, FINSEQ_1: 1;

              then i in ( dom (h | (n + 2))) by FINSEQ_1:def 3;

              then

               A94: ((h | (n + 2)) /. i) = p19 by FINSEQ_4: 70;

              

               A95: ( LSeg (h,(n + 2))) = ( LSeg (pn,pn1)) by A9, A44, Def3;

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

              then (i + 1) in ( Seg ( len (h | (n + 2)))) by A84, FINSEQ_1: 1;

              then (i + 1) in ( dom (h | (n + 2))) by FINSEQ_1:def 3;

              then

               A96: ((h | (n + 2)) /. (i + 1)) = p29 by FINSEQ_4: 70;

              (i + 1) <= ( len h) by A67, A84, A88, XXREAL_0: 2;

              

              then ( LSeg (h,i)) = ( LSeg (p19,p29)) by A83, Def3

              .= ( LSeg ((h | (n + 2)),i)) by A83, A84, A94, A96, Def3;

              then ( LSeg ((h | (n + 2)),i)) misses ( LSeg (pn,pn1)) by A91, A93, A95;

              hence contradiction by A77, A80, A82, XBOOLE_0: 3;

            end;

            then i = (n + 1) by A89, XXREAL_0: 1;

            then x in (( LSeg (h,(n + 1))) /\ ( LSeg (h,((n + 1) + 1)))) by A77, A80, A82, A90, A78, XBOOLE_0:def 4;

            hence thesis by A74, TARSKI:def 1;

          end;

          assume

           A97: x = pn;

          

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

          ((n + 1) + 1) <= ( len (h | (n + 2))) by A9, A11, FINSEQ_1: 59, XXREAL_0: 2;

          then

           A99: ( LSeg ((h | (n + 2)),(n + 1))) in { ( LSeg ((h | (n + 2)),i)) where i be Nat : 1 <= i & (i + 1) <= ( len (h | (n + 2))) } by A98;

          

           A100: (n + 2) in ( Seg (n + 2)) by A44, FINSEQ_1: 1;

          

           A101: ( len (h | (n + 2))) = (n + 2) by A9, A11, FINSEQ_1: 59, XXREAL_0: 2;

          then ( dom (h | (n + 2))) = ( Seg (n + 2)) by FINSEQ_1:def 3;

          then x = ((h | (n + 2)) /. ((n + 1) + 1)) by A97, A100, FINSEQ_4: 70;

          then x in ( LSeg ((h | (n + 2)),(n + 1))) by A101, A72, Th21;

          then

           A102: x in ( union { ( LSeg ((h | (n + 2)),i)) where i be Nat : 1 <= i & (i + 1) <= ( len (h | (n + 2))) }) by A99, TARSKI:def 4;

          x in ( LSeg (pn,pn1)) by A97, RLTOPSP1: 68;

          hence thesis by A102, XBOOLE_0:def 4;

        end;

        then ( Q(n) /\ ( LSeg (pn,pn1))) = {pn} by TARSKI:def 1;

        then

        consider hh be Function of I[01] , (( TOP-REAL 2) | NE1) such that

         A103: hh is being_homeomorphism and

         A104: (hh . 0 ) = (f . 0 ) and

         A105: (hh . 1) = (f1 . 1) by A12, A13, A71, A68, A69, TOPMETR2: 3;

        take hh;

        thus hh is being_homeomorphism & (hh . 0 ) = p1 & (hh . 1) = (h /. ((n + 1) + 2)) by A71, A70, A103, A104, A105;

      end;

      (h | 2) = (h | ( Seg 2)) by FINSEQ_1:def 15;

      

      then

       A106: ( dom (h | 2)) = (( dom h) /\ ( Seg 2)) by RELAT_1: 61

      .= (( Seg ( len h)) /\ ( Seg 2)) by FINSEQ_1:def 3

      .= ( Seg 2) by A2, FINSEQ_1: 7;

      then

       A107: ( len (h | 2)) = (1 + 1) by FINSEQ_1:def 3;

      then

       A108: 2 in ( Seg ( len (h | 2))) by FINSEQ_1: 1;

      

       A109: 1 in ( Seg ( len (h | 2))) by A107, FINSEQ_1: 1;

      now

        let x be object;

        

         A110: p2 = ((h | 2) /. 2) by A106, A107, A108, FINSEQ_4: 70;

        thus x in { ( LSeg ((h | 2),i)) where i be Nat : 1 <= i & (i + 1) <= ( len (h | 2)) } implies x = ( LSeg (h,1))

        proof

          assume x in { ( LSeg ((h | 2),i)) where i be Nat : 1 <= i & (i + 1) <= ( len (h | 2)) };

          then

          consider i be Nat such that

           A111: x = ( LSeg ((h | 2),i)) and

           A112: 1 <= i and

           A113: (i + 1) <= ( len (h | 2));

          (i + 1) <= (1 + 1) by A106, A113, FINSEQ_1:def 3;

          then i <= 1 by XREAL_1: 6;

          then

           A114: 1 = i by A112, XXREAL_0: 1;

          

           A115: ((h | 2) /. (1 + 1)) = (h /. (1 + 1)) by A106, A107, A108, FINSEQ_4: 70;

          ((h | 2) /. 1) = (h /. 1) by A106, A107, A109, FINSEQ_4: 70;

          

          hence x = ( LSeg (p1,p2)) by A107, A111, A114, A115, Def3

          .= ( LSeg (h,1)) by A2, Def3;

        end;

        assume x = ( LSeg (h,1));

        then

         A116: x = ( LSeg (p1,p2)) by A2, Def3;

        p1 = ((h | 2) /. 1) by A106, A107, A109, FINSEQ_4: 70;

        then x = ( LSeg ((h | 2),1)) by A107, A116, A110, Def3;

        hence x in { ( LSeg ((h | 2),i)) where i be Nat : 1 <= i & (i + 1) <= ( len (h | 2)) } by A107;

      end;

      then { ( LSeg ((h | 2),i)) where i be Nat : 1 <= i & (i + 1) <= ( len (h | 2)) } = {( LSeg (h,1))} by TARSKI:def 1;

      

      then

       A117: Q(0) = ( LSeg (h,1)) by ZFMISC_1: 25

      .= ( LSeg (p1,p2)) by A2, Def3;

      

       A118: (1 + 1) in ( Seg ( len h)) by A2, FINSEQ_1: 1;

      1 <= ( 0 + 2) & ( 0 + 2) <= ( len h) implies ex f be Function of I[01] , (( TOP-REAL 2) | ( LSeg (p1,p2))) st f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = (h /. ( 0 + 2))

      proof

        assume that 1 <= ( 0 + 2) and ( 0 + 2) <= ( len h);

        

         A119: 2 in ( dom h) by A118, FINSEQ_1:def 3;

        1 in ( dom h) by A3, FINSEQ_1:def 3;

        then ( LSeg (p1,p2)) is_an_arc_of (p1,p2) by A4, A119, Th9, PARTFUN2: 10;

        hence thesis;

      end;

      then

       A120: ARC[ 0 ] by A117;

      

       A121: for n holds ARC[n] from NAT_1:sch 2( A120, A5);

      (( len h) - 2) in NAT by A2, INT_1: 5;

      then

      reconsider h1 = (( len h) - 2) as Nat;

      1 <= (h1 + 2) by NAT_1: 12;

      then

      consider NE be non empty Subset of ( TOP-REAL 2) such that

       A122: NE = Q(h1) and

       A123: ex f be Function of I[01] , (( TOP-REAL 2) | NE) st f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = (h /. (h1 + 2)) by A121;

      consider f be Function of I[01] , (( TOP-REAL 2) | NE) such that

       A124: f is being_homeomorphism and

       A125: (f . 0 ) = p1 and

       A126: (f . 1) = (h /. (h1 + 2)) by A123;

      

       A127: (h | ( len h)) = (h | ( Seg ( len h))) by FINSEQ_1:def 15

      .= (h | ( dom h)) by FINSEQ_1:def 3

      .= h by RELAT_1: 68;

      then

      reconsider f as Function of I[01] , (( TOP-REAL 2) | P) by A122;

      take f;

      thus f is being_homeomorphism by A122, A124, A127;

      thus thesis by A125, A126;

    end;

    definition

      let P be Subset of ( TOP-REAL 2);

      :: TOPREAL1:def9

      attr P is being_S-P_arc means ex f st f is being_S-Seq & P = ( L~ f);

    end

    theorem :: TOPREAL1:26

    

     Th26: P1 is being_S-P_arc implies P1 <> {}

    proof

      assume P1 is being_S-P_arc;

      then

      consider f such that

       A1: f is being_S-Seq and

       A2: P1 = ( L~ f);

      ( len f) >= 2 by A1;

      hence thesis by A2, Th23;

    end;

    registration

      cluster being_S-P_arc -> non empty for Subset of ( TOP-REAL 2);

      coherence by Th26;

    end

    theorem :: TOPREAL1:27

    ex P1,P2 be non empty Subset of ( TOP-REAL 2) st P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = (P1 \/ P2) & (P1 /\ P2) = { |[ 0 , 0 ]|, |[1, 1]|}

    proof

      consider f1, f2 such that

       A1: f1 is being_S-Seq and

       A2: f2 is being_S-Seq and

       A3: R^2-unit_square = (( L~ f1) \/ ( L~ f2)) and

       A4: (( L~ f1) /\ ( L~ f2)) = { |[ 0 , 0 ]|, |[1, 1]|} and (f1 /. 1) = |[ 0 , 0 ]| and (f1 /. ( len f1)) = |[1, 1]| and (f2 /. 1) = |[ 0 , 0 ]| and (f2 /. ( len f2)) = |[1, 1]| by Th24;

      reconsider P1 = ( L~ f1), P2 = ( L~ f2) as non empty Subset of ( TOP-REAL 2) by A4;

      take P1, P2;

      thus thesis by A1, A2, A3, A4;

    end;

    theorem :: TOPREAL1:28

    

     Th28: P is being_S-P_arc implies ex p1, p2 st P is_an_arc_of (p1,p2)

    proof

      assume P is being_S-P_arc;

      then

      consider h such that

       A1: h is being_S-Seq and

       A2: P = ( L~ h);

      take (h /. 1), (h /. ( len h));

      thus thesis by A1, A2, Th25;

    end;

    theorem :: TOPREAL1:29

    P is being_S-P_arc implies ex f be Function of I[01] , (( TOP-REAL 2) | P) st f is being_homeomorphism

    proof

      assume P is being_S-P_arc;

      then

      consider p1, p2 such that

       A1: P is_an_arc_of (p1,p2) by Th28;

      ex f be Function of I[01] , (( TOP-REAL 2) | P) st f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = p2 by A1;

      hence thesis;

    end;

    scheme :: TOPREAL1:sch2

    TRSubsetEx { n() -> Nat , P[ object] } :

ex A be Subset of ( TOP-REAL n()) st for p be Point of ( TOP-REAL n()) holds p in A iff P[p];

      consider A be set such that

       A1: for x be object holds x in A iff x in the carrier of ( TOP-REAL n()) & P[x] from XBOOLE_0:sch 1;

      A c= the carrier of ( TOP-REAL n()) by A1;

      then

      reconsider A as Subset of ( TOP-REAL n());

      take A;

      thus thesis by A1;

    end;

    scheme :: TOPREAL1:sch3

    TRSubsetUniq { n() -> Nat , P[ object] } :

for A,B be Subset of ( TOP-REAL n()) st (for p be Point of ( TOP-REAL n()) holds p in A iff P[p]) & (for p be Point of ( TOP-REAL n()) holds p in B iff P[p]) holds A = B;

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

       A1: for p be Point of ( TOP-REAL n()) holds p in A iff P[p] and

       A2: for p be Point of ( TOP-REAL n()) holds p in B iff P[p];

      thus for x be object st x in A holds x in B by A2, A1;

      let x be object;

      assume

       A3: x in B;

      then P[x] by A2;

      hence thesis by A1, A3;

    end;

    definition

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

      :: TOPREAL1:def10

      func north_halfline p -> Subset of ( TOP-REAL 2) means

      : Def10: for x be Point of ( TOP-REAL 2) holds x in it iff (x `1 ) = (p `1 ) & (x `2 ) >= (p `2 );

      existence

      proof

        defpred P[ Point of ( TOP-REAL 2)] means ($1 `1 ) = (p `1 ) & ($1 `2 ) >= (p `2 );

        thus ex IT be Subset of ( TOP-REAL 2) st for x be Point of ( TOP-REAL 2) holds x in IT iff P[x] from TRSubsetEx;

      end;

      uniqueness

      proof

        defpred P[ Point of ( TOP-REAL 2)] means ($1 `1 ) = (p `1 ) & ($1 `2 ) >= (p `2 );

        thus for a,b be Subset of ( TOP-REAL 2) st (for x be Point of ( TOP-REAL 2) holds x in a iff P[x]) & (for x be Point of ( TOP-REAL 2) holds x in b iff P[x]) holds a = b from TRSubsetUniq;

      end;

      :: TOPREAL1:def11

      func east_halfline p -> Subset of ( TOP-REAL 2) means

      : Def11: for x be Point of ( TOP-REAL 2) holds x in it iff (x `1 ) >= (p `1 ) & (x `2 ) = (p `2 );

      existence

      proof

        defpred P[ Point of ( TOP-REAL 2)] means ($1 `1 ) >= (p `1 ) & ($1 `2 ) = (p `2 );

        thus ex IT be Subset of ( TOP-REAL 2) st for x be Point of ( TOP-REAL 2) holds x in IT iff P[x] from TRSubsetEx;

      end;

      uniqueness

      proof

        defpred P[ Point of ( TOP-REAL 2)] means ($1 `1 ) >= (p `1 ) & ($1 `2 ) = (p `2 );

        thus for a,b be Subset of ( TOP-REAL 2) st (for x be Point of ( TOP-REAL 2) holds x in a iff P[x]) & (for x be Point of ( TOP-REAL 2) holds x in b iff P[x]) holds a = b from TRSubsetUniq;

      end;

      :: TOPREAL1:def12

      func south_halfline p -> Subset of ( TOP-REAL 2) means

      : Def12: for x be Point of ( TOP-REAL 2) holds x in it iff (x `1 ) = (p `1 ) & (x `2 ) <= (p `2 );

      existence

      proof

        defpred P[ Point of ( TOP-REAL 2)] means ($1 `1 ) = (p `1 ) & ($1 `2 ) <= (p `2 );

        thus ex IT be Subset of ( TOP-REAL 2) st for x be Point of ( TOP-REAL 2) holds x in IT iff P[x] from TRSubsetEx;

      end;

      uniqueness

      proof

        defpred P[ Point of ( TOP-REAL 2)] means ($1 `1 ) = (p `1 ) & ($1 `2 ) <= (p `2 );

        thus for a,b be Subset of ( TOP-REAL 2) st (for x be Point of ( TOP-REAL 2) holds x in a iff P[x]) & (for x be Point of ( TOP-REAL 2) holds x in b iff P[x]) holds a = b from TRSubsetUniq;

      end;

      :: TOPREAL1:def13

      func west_halfline p -> Subset of ( TOP-REAL 2) means

      : Def13: for x be Point of ( TOP-REAL 2) holds x in it iff (x `1 ) <= (p `1 ) & (x `2 ) = (p `2 );

      existence

      proof

        defpred P[ Point of ( TOP-REAL 2)] means ($1 `1 ) <= (p `1 ) & ($1 `2 ) = (p `2 );

        thus ex IT be Subset of ( TOP-REAL 2) st for x be Point of ( TOP-REAL 2) holds x in IT iff P[x] from TRSubsetEx;

      end;

      uniqueness

      proof

        defpred P[ Point of ( TOP-REAL 2)] means ($1 `1 ) <= (p `1 ) & ($1 `2 ) = (p `2 );

        thus for a,b be Subset of ( TOP-REAL 2) st (for x be Point of ( TOP-REAL 2) holds x in a iff P[x]) & (for x be Point of ( TOP-REAL 2) holds x in b iff P[x]) holds a = b from TRSubsetUniq;

      end;

    end

    theorem :: TOPREAL1:30

    ( north_halfline p) = { q where q be Point of ( TOP-REAL 2) : (q `1 ) = (p `1 ) & (q `2 ) >= (p `2 ) }

    proof

      set A = { q where q be Point of ( TOP-REAL 2) : (q `1 ) = (p `1 ) & (q `2 ) >= (p `2 ) };

      hereby

        let x be object;

        assume

         A1: x in ( north_halfline p);

        then

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

        

         A2: (q `2 ) >= (p `2 ) by A1, Def10;

        (q `1 ) = (p `1 ) by A1, Def10;

        hence x in A by A2;

      end;

      let x be object;

      assume x in A;

      then ex q be Point of ( TOP-REAL 2) st x = q & (q `1 ) = (p `1 ) & (q `2 ) >= (p `2 );

      hence thesis by Def10;

    end;

    theorem :: TOPREAL1:31

    

     Th31: ( north_halfline p) = { |[(p `1 ), r]| where r be Real : r >= (p `2 ) }

    proof

      set A = { |[(p `1 ), r]| where r be Real : r >= (p `2 ) };

      hereby

        let x be object;

        assume

         A1: x in ( north_halfline p);

        then

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

        

         A2: (q `2 ) >= (p `2 ) by A1, Def10;

        

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

        (q `1 ) = (p `1 ) by A1, Def10;

        hence x in A by A2, A3;

      end;

      let x be object;

      assume x in A;

      then

      consider r be Real such that

       A4: x = |[(p `1 ), r]| and

       A5: r >= (p `2 );

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

      

       A6: (q `2 ) = r by A4, EUCLID: 52;

      (q `1 ) = (p `1 ) by A4, EUCLID: 52;

      hence thesis by A5, A6, Def10;

    end;

    theorem :: TOPREAL1:32

    ( east_halfline p) = { q where q be Point of ( TOP-REAL 2) : (q `1 ) >= (p `1 ) & (q `2 ) = (p `2 ) }

    proof

      set A = { q where q be Point of ( TOP-REAL 2) : (q `1 ) >= (p `1 ) & (q `2 ) = (p `2 ) };

      hereby

        let x be object;

        assume

         A1: x in ( east_halfline p);

        then

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

        

         A2: (q `2 ) = (p `2 ) by A1, Def11;

        (q `1 ) >= (p `1 ) by A1, Def11;

        hence x in A by A2;

      end;

      let x be object;

      assume x in A;

      then ex q be Point of ( TOP-REAL 2) st x = q & (q `1 ) >= (p `1 ) & (q `2 ) = (p `2 );

      hence thesis by Def11;

    end;

    theorem :: TOPREAL1:33

    

     Th33: ( east_halfline p) = { |[r, (p `2 )]| where r be Real : r >= (p `1 ) }

    proof

      set A = { |[r, (p `2 )]| where r be Real : r >= (p `1 ) };

      hereby

        let x be object;

        assume

         A1: x in ( east_halfline p);

        then

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

        

         A2: (q `2 ) = (p `2 ) by A1, Def11;

        

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

        (q `1 ) >= (p `1 ) by A1, Def11;

        hence x in A by A2, A3;

      end;

      let x be object;

      assume x in A;

      then

      consider r be Real such that

       A4: x = |[r, (p `2 )]| and

       A5: r >= (p `1 );

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

      

       A6: (q `2 ) = (p `2 ) by A4, EUCLID: 52;

      (q `1 ) = r by A4, EUCLID: 52;

      hence thesis by A5, A6, Def11;

    end;

    theorem :: TOPREAL1:34

    ( south_halfline p) = { q where q be Point of ( TOP-REAL 2) : (q `1 ) = (p `1 ) & (q `2 ) <= (p `2 ) }

    proof

      set A = { q where q be Point of ( TOP-REAL 2) : (q `1 ) = (p `1 ) & (q `2 ) <= (p `2 ) };

      hereby

        let x be object;

        assume

         A1: x in ( south_halfline p);

        then

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

        

         A2: (q `2 ) <= (p `2 ) by A1, Def12;

        (q `1 ) = (p `1 ) by A1, Def12;

        hence x in A by A2;

      end;

      let x be object;

      assume x in A;

      then ex q be Point of ( TOP-REAL 2) st x = q & (q `1 ) = (p `1 ) & (q `2 ) <= (p `2 );

      hence thesis by Def12;

    end;

    theorem :: TOPREAL1:35

    

     Th35: ( south_halfline p) = { |[(p `1 ), r]| where r be Real : r <= (p `2 ) }

    proof

      set A = { |[(p `1 ), r]| where r be Real : r <= (p `2 ) };

      hereby

        let x be object;

        assume

         A1: x in ( south_halfline p);

        then

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

        

         A2: (q `2 ) <= (p `2 ) by A1, Def12;

        

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

        (q `1 ) = (p `1 ) by A1, Def12;

        hence x in A by A2, A3;

      end;

      let x be object;

      assume x in A;

      then

      consider r be Real such that

       A4: x = |[(p `1 ), r]| and

       A5: r <= (p `2 );

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

      

       A6: (q `2 ) = r by A4, EUCLID: 52;

      (q `1 ) = (p `1 ) by A4, EUCLID: 52;

      hence thesis by A5, A6, Def12;

    end;

    theorem :: TOPREAL1:36

    ( west_halfline p) = { q where q be Point of ( TOP-REAL 2) : (q `1 ) <= (p `1 ) & (q `2 ) = (p `2 ) }

    proof

      set A = { q where q be Point of ( TOP-REAL 2) : (q `1 ) <= (p `1 ) & (q `2 ) = (p `2 ) };

      hereby

        let x be object;

        assume

         A1: x in ( west_halfline p);

        then

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

        

         A2: (q `2 ) = (p `2 ) by A1, Def13;

        (q `1 ) <= (p `1 ) by A1, Def13;

        hence x in A by A2;

      end;

      let x be object;

      assume x in A;

      then ex q be Point of ( TOP-REAL 2) st x = q & (q `1 ) <= (p `1 ) & (q `2 ) = (p `2 );

      hence thesis by Def13;

    end;

    theorem :: TOPREAL1:37

    

     Th37: ( west_halfline p) = { |[r, (p `2 )]| where r be Real : r <= (p `1 ) }

    proof

      set A = { |[r, (p `2 )]| where r be Real : r <= (p `1 ) };

      hereby

        let x be object;

        assume

         A1: x in ( west_halfline p);

        then

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

        

         A2: (q `2 ) = (p `2 ) by A1, Def13;

        

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

        (q `1 ) <= (p `1 ) by A1, Def13;

        hence x in A by A2, A3;

      end;

      let x be object;

      assume x in A;

      then

      consider r be Real such that

       A4: x = |[r, (p `2 )]| and

       A5: r <= (p `1 );

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

      

       A6: (q `2 ) = (p `2 ) by A4, EUCLID: 52;

      (q `1 ) = r by A4, EUCLID: 52;

      hence thesis by A5, A6, Def13;

    end;

    registration

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

      cluster ( north_halfline p) -> non empty;

      coherence

      proof

        ( north_halfline p) = { |[(p `1 ), r]| where r be Real : r >= (p `2 ) } by Th31;

        then |[(p `1 ), (p `2 )]| in ( north_halfline p);

        hence thesis;

      end;

      cluster ( east_halfline p) -> non empty;

      coherence

      proof

        ( east_halfline p) = { |[r, (p `2 )]| where r be Real : r >= (p `1 ) } by Th33;

        then |[(p `1 ), (p `2 )]| in ( east_halfline p);

        hence thesis;

      end;

      cluster ( south_halfline p) -> non empty;

      coherence

      proof

        ( south_halfline p) = { |[(p `1 ), r]| where r be Real : r <= (p `2 ) } by Th35;

        then |[(p `1 ), (p `2 )]| in ( south_halfline p);

        hence thesis;

      end;

      cluster ( west_halfline p) -> non empty;

      coherence

      proof

        ( west_halfline p) = { |[r, (p `2 )]| where r be Real : r <= (p `1 ) } by Th37;

        then |[(p `1 ), (p `2 )]| in ( west_halfline p);

        hence thesis;

      end;

    end

    theorem :: TOPREAL1:38

    p in ( west_halfline p) & p in ( east_halfline p) & p in ( north_halfline p) & p in ( south_halfline p)

    proof

      

       A1: (p `2 ) = (p `2 );

      (p `1 ) <= (p `1 );

      hence thesis by A1, Def10, Def11, Def12, Def13;

    end;