topreal6.miz



    begin

    reserve a,b for Real,

r for Real,

rr for Real,

i,j,n for Nat,

M for non empty MetrSpace,

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

e for Point of ( Euclid 2),

w for Point of ( Euclid n),

z for Point of M,

A,B for Subset of ( TOP-REAL n),

P for Subset of ( TOP-REAL 2),

D for non empty Subset of ( TOP-REAL 2);

    ::$Canceled

    theorem :: TOPREAL6:2

    

     Th1: 0 <= a & a <= b implies |.a.| <= |.b.|

    proof

      assume that

       A1: 0 <= a and

       A2: a <= b;

       |.a.| = a by A1, ABSVALUE:def 1;

      hence thesis by A1, A2, ABSVALUE:def 1;

    end;

    theorem :: TOPREAL6:3

    

     Th2: b <= a & a <= 0 implies |.a.| <= |.b.|

    proof

      assume that

       A1: b <= a and

       A2: a <= 0 ;

      per cases by A2;

        suppose a = 0 ;

        then |.a.| = 0 by ABSVALUE: 2;

        hence thesis by COMPLEX1: 46;

      end;

        suppose

         A3: a < 0 ;

        then

         A4: |.a.| = ( - a) by ABSVALUE:def 1;

         |.b.| = ( - b) by A1, A3, ABSVALUE:def 1;

        hence thesis by A1, A4, XREAL_1: 24;

      end;

    end;

    theorem :: TOPREAL6:4

    ( Product ( 0 |-> rr)) = 1 by RVSUM_1: 94;

    theorem :: TOPREAL6:5

    

     Th4: ( Product (1 |-> rr)) = rr

    proof

      

      thus ( Product (1 |-> rr)) = ( Product <*rr*>) by FINSEQ_2: 59

      .= rr;

    end;

    theorem :: TOPREAL6:6

    ( Product (2 |-> rr)) = (rr * rr)

    proof

      

      thus ( Product (2 |-> rr)) = ( Product <*rr, rr*>) by FINSEQ_2: 61

      .= (rr * rr) by RVSUM_1: 99;

    end;

    theorem :: TOPREAL6:7

    

     Th6: ( Product ((n + 1) |-> rr)) = (( Product (n |-> rr)) * rr)

    proof

      

      thus ( Product ((n + 1) |-> rr)) = (( Product (n |-> rr)) * ( Product (1 |-> rr))) by RVSUM_1: 104

      .= (( Product (n |-> rr)) * rr) by Th4;

    end;

    theorem :: TOPREAL6:8

    

     Th7: j <> 0 & rr = 0 iff ( Product (j |-> rr)) = 0

    proof

      set f = (j |-> rr);

      

       A1: ( dom f) = ( Seg j) by FUNCOP_1: 13;

      hereby

        assume that

         A2: j <> 0 and

         A3: rr = 0 ;

        ex n be Nat st j = (n + 1) by A2, NAT_1: 6;

        then 1 <= j by NAT_1: 11;

        then

         A4: 1 in ( Seg j) by FINSEQ_1: 1;

        then (f . 1) = 0 by A3, FUNCOP_1: 7;

        hence ( Product f) = 0 by A1, A4, RVSUM_1: 103;

      end;

      assume ( Product f) = 0 ;

      then ex n be Nat st n in ( dom f) & (f . n) = 0 by RVSUM_1: 103;

      hence thesis by A1, FUNCOP_1: 7;

    end;

    theorem :: TOPREAL6:9

    

     Th8: rr <> 0 & j <= i implies ( Product ((i -' j) |-> rr)) = (( Product (i |-> rr)) / ( Product (j |-> rr)))

    proof

      assume that

       A1: rr <> 0 and

       A2: j <= i;

      defpred P[ Nat] means j <= $1 implies ( Product (($1 -' j) |-> rr)) = (( Product ($1 |-> rr)) / ( Product (j |-> rr)));

      

       A3: ( Product (j |-> rr)) <> 0 by A1, Th7;

      

       A4: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume that

         A5: P[n] and

         A6: j <= (n + 1);

        per cases by A6, NAT_1: 8;

          suppose

           A7: j <= n;

          ( Product (((n -' j) + 1) |-> rr)) = (( Product ((n -' j) |-> rr)) * ( Product (1 |-> rr))) by RVSUM_1: 104

          .= ((( Product (n |-> rr)) / ( Product (j |-> rr))) * rr) by A5, A7, Th4

          .= ((( Product (n |-> rr)) * rr) / ( Product (j |-> rr))) by XCMPLX_1: 74

          .= (( Product ((n + 1) |-> rr)) / ( Product (j |-> rr))) by Th6;

          hence thesis by A7, NAT_D: 38;

        end;

          suppose

           A8: j = (n + 1);

          

          hence ( Product (((n + 1) -' j) |-> rr)) = ( Product ( 0 |-> rr)) by XREAL_1: 232

          .= 1 by RVSUM_1: 94

          .= (( Product ((n + 1) |-> rr)) / ( Product (j |-> rr))) by A3, A8, XCMPLX_1: 60;

        end;

      end;

      

       A9: P[ 0 ]

      proof

        assume

         A10: j <= 0 ;

        then j = 0 ;

        

        hence ( Product (( 0 -' j) |-> rr)) = (( Product ( 0 |-> rr)) / ( Product ( <*> REAL ))) by NAT_D: 40, RVSUM_1: 94

        .= (( Product ( 0 |-> rr)) / ( Product (j |-> rr))) by A10;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A9, A4);

      hence thesis by A2;

    end;

    theorem :: TOPREAL6:10

    r <> 0 & j <= i implies (r |^ (i -' j)) = ((r |^ i) / (r |^ j))

    proof

      assume that

       A1: r <> 0 and

       A2: j <= i;

      reconsider rr = r as Real;

      

      thus ((r |^ i) / (r |^ j)) = (( Product (i |-> rr)) / (rr |^ j)) by NEWTON:def 1

      .= (( Product (i |-> rr)) / ( Product (j |-> rr))) by NEWTON:def 1

      .= ( Product ((i -' j) |-> rr)) by A1, A2, Th8

      .= (r |^ (i -' j)) by NEWTON:def 1;

    end;

    reserve a,b for Real;

    theorem :: TOPREAL6:11

    

     Th10: for a,b be Real holds ( sqr <*a, b*>) = <*(a ^2 ), (b ^2 )*>

    proof

      let a,b be Real;

      ( dom sqrreal ) = REAL by FUNCT_2:def 1;

      then

       A1: ( rng <*a, b*>) c= ( dom sqrreal );

      

       A2: ( dom <*(a ^2 ), (b ^2 )*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      

       A3: for i be object st i in ( dom <*(a ^2 ), (b ^2 )*>) holds (( sqr <*a, b*>) . i) = ( <*(a ^2 ), (b ^2 )*> . i)

      proof

        let i be object;

        

         A4: ( <*a, b*> . 1) = a by FINSEQ_1: 44;

        

         A5: ( <*a, b*> . 2) = b by FINSEQ_1: 44;

        assume

         A6: i in ( dom <*(a ^2 ), (b ^2 )*>);

        per cases by A2, A6, TARSKI:def 2;

          suppose

           A7: i = 1;

          

          hence (( sqr <*a, b*>) . i) = (a ^2 ) by A4, VALUED_1: 11

          .= ( <*(a ^2 ), (b ^2 )*> . i) by A7, FINSEQ_1: 44;

        end;

          suppose

           A8: i = 2;

          

          hence (( sqr <*a, b*>) . i) = (b ^2 ) by A5, VALUED_1: 11

          .= ( <*(a ^2 ), (b ^2 )*> . i) by A8, FINSEQ_1: 44;

        end;

      end;

      ( dom ( sqr <*a, b*>)) = ( dom ( sqrreal * <*a, b*>)) by RVSUM_1:def 8

      .= ( dom <*a, b*>) by A1, RELAT_1: 27

      .= {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      hence thesis by A3, FINSEQ_1: 2, FINSEQ_1: 89, FUNCT_1: 2;

    end;

    theorem :: TOPREAL6:12

    

     Th11: for i be Nat holds for F be FinSequence of REAL st i in ( dom ( abs F)) & a = (F . i) holds (( abs F) . i) = |.a.|

    proof

      let i be Nat;

      let F be FinSequence of REAL such that

       A1: i in ( dom ( abs F)) and

       A2: a = (F . i);

      (( abs F) . i) = ( absreal . a) by A1, A2, FUNCT_1: 12;

      hence thesis by EUCLID:def 2;

    end;

    theorem :: TOPREAL6:13

    for a,b be Real holds ( abs <*a, b*>) = <* |.a.|, |.b.|*>

    proof

      let a,b be Real;

      ( dom absreal ) = REAL by FUNCT_2:def 1;

      then ( rng <*a, b*>) c= ( dom absreal );

      

      then

       A1: ( dom ( abs <*a, b*>)) = ( dom <*a, b*>) by RELAT_1: 27

      .= {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      

       A2: ( dom <* |.a.|, |.b.|*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      reconsider a, b as Element of REAL by XREAL_0:def 1;

      for i be object st i in ( dom <* |.a.|, |.b.|*>) holds (( abs <*a, b*>) . i) = ( <* |.a.|, |.b.|*> . i)

      proof

        let i be object;

        

         A3: ( <*a, b*> . 1) = a by FINSEQ_1: 44;

        

         A4: ( <*a, b*> . 2) = b by FINSEQ_1: 44;

        

         A5: 2 in {1, 2} by TARSKI:def 2;

        

         A6: 1 in {1, 2} by TARSKI:def 2;

        assume

         A7: i in ( dom <* |.a.|, |.b.|*>);

        per cases by A2, A7, TARSKI:def 2;

          suppose

           A8: i = 1;

          

          hence (( abs <*a, b*>) . i) = |.a.| by A1, A3, A6, Th11

          .= ( <* |.a.|, |.b.|*> . i) by A8, FINSEQ_1: 44;

        end;

          suppose

           A9: i = 2;

          

          hence (( abs <*a, b*>) . i) = |.b.| by A1, A4, A5, Th11

          .= ( <* |.a.|, |.b.|*> . i) by A9, FINSEQ_1: 44;

        end;

      end;

      hence thesis by A1, FINSEQ_1: 2, FINSEQ_1: 89, FUNCT_1: 2;

    end;

    reserve a,b for Real;

    theorem :: TOPREAL6:14

    for a,b,c,d be Real st a <= b & c <= d holds ( |.(b - a).| + |.(d - c).|) = ((b - a) + (d - c))

    proof

      let a,b,c,d be Real;

      assume that

       A1: a <= b and

       A2: c <= d;

      (a - a) <= (b - a) by A1, XREAL_1: 13;

      then

       A3: |.(b - a).| = (b - a) by ABSVALUE:def 1;

      (c - c) <= (d - c) by A2, XREAL_1: 13;

      hence thesis by A3, ABSVALUE:def 1;

    end;

    theorem :: TOPREAL6:15

    

     Th14: for a,r be Real holds r > 0 implies a in ].(a - r), (a + r).[

    proof

      let a,r be Real;

      assume r > 0 ;

      then |.(a - a).| < r by ABSVALUE:def 1;

      hence thesis by RCOMP_1: 1;

    end;

    theorem :: TOPREAL6:16

    for a,r be Real holds r >= 0 implies a in [.(a - r), (a + r).]

    proof

      let a,r be Real;

      assume

       A1: r >= 0 ;

      reconsider a, r as Real;

      

       A2: (a + 0 ) <= (a + r) by A1, XREAL_1: 7;

      reconsider amr = (a - r), apr = (a + r) as Real;

      reconsider X = [.amr, apr.] as Subset of REAL ;

      

       A3: X = { b where b be Real : amr <= b & b <= apr } by RCOMP_1:def 1;

      (a - r) <= (a - 0 ) by A1, XREAL_1: 13;

      hence thesis by A3, A2;

    end;

    theorem :: TOPREAL6:17

    

     Th16: for a,b be Real holds a < b implies ( lower_bound ].a, b.[) = a & ( upper_bound ].a, b.[) = b

    proof

      let a,b be Real;

      assume

       A1: a < b;

      set X = ].a, b.[;

      reconsider a, b as Real;

      

       A2: ((a + b) / 2) < b by A1, XREAL_1: 226;

      

       A3: a < ((a + b) / 2) by A1, XREAL_1: 226;

      then

       A4: ((a + b) / 2) in { l where l be Real : a < l & l < b } by A2;

      

       A5: for s be Real st 0 < s holds ex r be Real st r in X & r < (a + s)

      proof

        let s be Real such that

         A6: 0 < s and

         A7: for r be Real st r in X holds r >= (a + s);

        reconsider s as Real;

        per cases ;

          suppose

           A8: (a + s) >= b;

          

           A9: ((a + b) / 2) in X by A4, RCOMP_1:def 2;

          ((a + b) / 2) < (a + s) by A2, A8, XXREAL_0: 2;

          hence thesis by A7, A9;

        end;

          suppose

           A10: (a + s) < b;

          

           A11: a < (a + s) by A6, XREAL_1: 29;

          then ((a + (a + s)) / 2) < (a + s) by XREAL_1: 226;

          then

           A12: ((a + (a + s)) / 2) < b by A10, XXREAL_0: 2;

          a < ((a + (a + s)) / 2) by A11, XREAL_1: 226;

          then ((a + (a + s)) / 2) in { r : a < r & r < b } by A12;

          then ((a + (a + s)) / 2) in X by RCOMP_1:def 2;

          hence thesis by A7, A11, XREAL_1: 226;

        end;

      end;

      

       A13: for s be Real st 0 < s holds ex r be Real st r in X & (b - s) < r

      proof

        let s be Real such that

         A14: 0 < s and

         A15: for r be Real st r in X holds r <= (b - s);

        reconsider s as Real;

        per cases ;

          suppose

           A16: (b - s) <= a;

          

           A17: ((a + b) / 2) in X by A4, RCOMP_1:def 2;

          ((a + b) / 2) > (b - s) by A3, A16, XXREAL_0: 2;

          hence thesis by A15, A17;

        end;

          suppose

           A18: (b - s) > a;

          

           A19: (b - s) < (b - 0 ) by A14, XREAL_1: 15;

          then (b - s) < ((b + (b - s)) / 2) by XREAL_1: 226;

          then

           A20: a < ((b + (b - s)) / 2) by A18, XXREAL_0: 2;

          ((b + (b - s)) / 2) < b by A19, XREAL_1: 226;

          then ((b + (b - s)) / 2) in { r : a < r & r < b } by A20;

          then ((b + (b - s)) / 2) in X by RCOMP_1:def 2;

          hence thesis by A15, A19, XREAL_1: 226;

        end;

      end;

      a is LowerBound of X

      proof

        let r be ExtReal;

        assume r in X;

        then r in { l where l be Real : a < l & l < b } by RCOMP_1:def 2;

        then ex r1 be Real st r1 = r & a < r1 & r1 < b;

        hence thesis;

      end;

      then

       A21: X is bounded_below;

      

       A22: for r be Real st r in X holds a <= r

      proof

        let r be Real;

        assume r in X;

        then r in { l where l be Real : a < l & l < b } by RCOMP_1:def 2;

        then ex r1 be Real st r1 = r & a < r1 & r1 < b;

        hence thesis;

      end;

      b is UpperBound of X

      proof

        let r be ExtReal;

        assume r in X;

        then r in { l where l be Real : a < l & l < b } by RCOMP_1:def 2;

        then ex r1 be Real st r1 = r & a < r1 & r1 < b;

        hence thesis;

      end;

      then

       A23: X is bounded_above;

      

       A24: for r be Real st r in X holds b >= r

      proof

        let r be Real;

        assume r in X;

        then r in { l where l be Real : a < l & l < b } by RCOMP_1:def 2;

        then ex r1 be Real st r1 = r & a < r1 & r1 < b;

        hence thesis;

      end;

      ((a + b) / 2) in X by A4, RCOMP_1:def 2;

      hence thesis by A21, A23, A22, A5, A24, A13, SEQ_4:def 1, SEQ_4:def 2;

    end;

    begin

    registration

      let T be TopStruct, A be finite Subset of T;

      cluster (T | A) -> finite;

      coherence by PRE_TOPC: 8;

    end

    registration

      let T be TopStruct;

      cluster empty -> connected for Subset of T;

      coherence

      proof

        let C be Subset of T;

        assume C is empty;

        then

        reconsider D = C as empty Subset of T;

        let A,B be Subset of (T | C) such that ( [#] (T | C)) = (A \/ B) and (A,B) are_separated ;

        ( [#] (T | D)) = {} ;

        hence thesis;

      end;

    end

    ::$Canceled

    theorem :: TOPREAL6:19

    

     Th17: for S,T be TopSpace st (S,T) are_homeomorphic & S is connected holds T is connected

    proof

      let S,T be TopSpace;

      given f be Function of S, T such that

       A1: f is being_homeomorphism;

      

       A2: ( rng f) = ( [#] T) by A1;

      assume

       A3: S is connected;

      ( dom f) = ( [#] S) by A1;

      then (f .: ( [#] S)) = ( [#] T) by A2, RELAT_1: 113;

      hence thesis by A1, A3, CONNSP_1: 14;

    end;

    theorem :: TOPREAL6:20

    for T be TopSpace, F be finite Subset-Family of T st for X be Subset of T st X in F holds X is compact holds ( union F) is compact

    proof

      let T be TopSpace, F be finite Subset-Family of T such that

       A1: for X be Subset of T st X in F holds X is compact;

      defpred P[ set] means ex A be Subset of T st A = ( union $1) & A is compact;

      

       A2: for x,B be set st x in F & B c= F & P[B] holds P[(B \/ {x})]

      proof

        let x,B be set such that

         A3: x in F and

         A4: B c= F;

        B c= ( bool the carrier of T)

        proof

          let b be object;

          assume b in B;

          then b in F by A4;

          hence thesis;

        end;

        then

        reconsider C = B as Subset-Family of T;

        reconsider X = x as Subset of T by A3;

        given A be Subset of T such that

         A5: A = ( union B) and

         A6: A is compact;

        set K = (( union C) \/ X);

        take K;

        ( union {x}) = x by ZFMISC_1: 25;

        hence K = ( union (B \/ {x})) by ZFMISC_1: 78;

        X is compact by A1, A3;

        hence thesis by A5, A6, COMPTS_1: 10;

      end;

      

       A7: P[ {} ]

      proof

        take ( {} T);

        thus thesis by ZFMISC_1: 2;

      end;

      

       A8: F is finite;

       P[F] from FINSET_1:sch 2( A8, A7, A2);

      hence thesis;

    end;

    begin

    theorem :: TOPREAL6:21

    

     Th19: for A,B,C,D be set, a,b be object st A c= B & C c= D holds ( product ((a,b) --> (A,C))) c= ( product ((a,b) --> (B,D)))

    proof

      let A,B,C,D be set, a,b be object such that

       A1: A c= B and

       A2: C c= D;

      set f = ((a,b) --> (A,C)), g = ((a,b) --> (B,D));

      

       A3: ( dom f) = {a, b} by FUNCT_4: 62;

      

       A4: for x be object st x in ( dom f) holds (f . x) c= (g . x)

      proof

        let x be object;

        assume x in ( dom f);

        then

         A5: x = a or x = b by A3, TARSKI:def 2;

        per cases ;

          suppose

           A6: a <> b;

          

           A7: (f . b) = C by FUNCT_4: 63;

          (f . a) = A by A6, FUNCT_4: 63;

          hence thesis by A1, A2, A5, A6, A7, FUNCT_4: 63;

        end;

          suppose

           A8: a = b;

          then f = (a .--> C) by FUNCT_4: 81;

          then

           A9: (f . a) = C by FUNCOP_1: 72;

          g = (a .--> D) by A8, FUNCT_4: 81;

          hence thesis by A2, A5, A8, A9, FUNCOP_1: 72;

        end;

      end;

      ( dom g) = {a, b} by FUNCT_4: 62;

      hence thesis by A4, CARD_3: 27, FUNCT_4: 62;

    end;

    theorem :: TOPREAL6:22

    

     Th20: for A,B be Subset of REAL holds ( product ((1,2) --> (A,B))) is Subset of ( TOP-REAL 2)

    proof

      let A,B be Subset of REAL ;

      set f = ((1,2) --> (A,B));

      ( product f) c= the carrier of ( TOP-REAL 2)

      proof

        let a be object;

        

         A1: (f . 1) = A by FUNCT_4: 63;

        

         A2: (f . 2) = B by FUNCT_4: 63;

        assume a in ( product f);

        then

        consider g be Function such that

         A3: a = g and

         A4: ( dom g) = ( dom f) and

         A5: for x be object st x in ( dom f) holds (g . x) in (f . x) by CARD_3:def 5;

        

         A6: ( dom f) = {1, 2} by FUNCT_4: 62;

        then 2 in ( dom f) by TARSKI:def 2;

        then

         A7: (g . 2) in B by A5, A2;

        1 in ( dom f) by A6, TARSKI:def 2;

        then (g . 1) in A by A5, A1;

        then

        reconsider m = (g . 1), n = (g . 2) as Real by A7;

         A8:

        now

          let k be object;

          assume k in ( dom g);

          then k = 1 or k = 2 by A4, TARSKI:def 2;

          hence (g . k) = ( <*(g . 1), (g . 2)*> . k) by FINSEQ_1: 44;

        end;

        ( dom <*(g . 1), (g . 2)*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

        then a = |[m, n]| by A3, A4, A8, FUNCT_1: 2, FUNCT_4: 62;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: TOPREAL6:23

     |. |[ 0 , a]|.| = |.a.| & |. |[a, 0 ]|.| = |.a.|

    proof

      reconsider aa = a as Real;

      reconsider a2 = (aa ^2 ), z2 = ( 0 ^2 ) as Real;

       |. <* 0 , aa*>.| = ( sqrt ( Sum <*z2, a2*>)) by Th10

      .= ( sqrt ( 0 + (a ^2 ))) by RVSUM_1: 77

      .= |.a.| by COMPLEX1: 72;

      hence |. |[ 0 , a]|.| = |.a.|;

       |. <*aa, 0 *>.| = ( sqrt ( Sum <*a2, z2*>)) by Th10

      .= ( sqrt ((a ^2 ) + 0 )) by RVSUM_1: 77

      .= |.a.| by COMPLEX1: 72;

      hence thesis;

    end;

    theorem :: TOPREAL6:24

    

     Th22: for p be Point of ( Euclid 2), q be Point of ( TOP-REAL 2) st p = ( 0. ( TOP-REAL 2)) & p = q holds q = <* 0 , 0 *> & (q `1 ) = 0 & (q `2 ) = 0

    proof

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

       A1: p = ( 0. ( TOP-REAL 2)) and

       A2: p = q;

      ( 0.REAL 2) = ( 0. ( TOP-REAL 2)) by EUCLID: 66;

      then p = <* 0 , 0 *> by A1, FINSEQ_2: 61;

      hence thesis by A2, EUCLID: 52;

    end;

    theorem :: TOPREAL6:25

    for p,q be Point of ( Euclid 2), z be Point of ( TOP-REAL 2) st p = ( 0.REAL 2) & q = z holds ( dist (p,q)) = |.z.|

    proof

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

       A1: p = ( 0.REAL 2) and

       A2: q = z;

      reconsider P = p as Point of ( TOP-REAL 2) by TOPREAL3: 8;

      

       A3: ( 0.REAL 2) = ( 0. ( TOP-REAL 2)) by EUCLID: 66;

      then

       A4: (P `1 ) = 0 by A1, Th22;

      

       A5: (P `2 ) = 0 by A1, A3, Th22;

      ( dist (p,q)) = (( Pitag_dist 2) . (p,q)) by METRIC_1:def 1

      .= ( sqrt ((((P `1 ) - (z `1 )) ^2 ) + (((P `2 ) - (z `2 )) ^2 ))) by A2, TOPREAL3: 7

      .= ( sqrt (((z `1 ) ^2 ) + ((z `2 ) ^2 ))) by A4, A5;

      hence thesis by JGRAPH_1: 30;

    end;

    theorem :: TOPREAL6:26

    

     Th24: (r * p) = |[(r * (p `1 )), (r * (p `2 ))]|

    proof

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

      hence thesis by EUCLID: 58;

    end;

    theorem :: TOPREAL6:27

    

     Th25: s = (((1 - r) * p) + (r * q)) & s <> p & 0 <= r implies 0 < r

    proof

      assume that

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

       A2: s <> p and

       A3: 0 <= r;

      assume

       A4: r <= 0 ;

      

      then s = (((1 - 0 ) * p) + (r * q)) by A1, A3

      .= (((1 - 0 ) * p) + ( 0 * q)) by A3, A4

      .= ((1 * p) + ( 0. ( TOP-REAL 2))) by RLVECT_1: 10

      .= (1 * p) by RLVECT_1: 4

      .= p by RLVECT_1:def 8;

      hence thesis by A2;

    end;

    theorem :: TOPREAL6:28

    

     Th26: s = (((1 - r) * p) + (r * q)) & s <> q & r <= 1 implies r < 1

    proof

      assume that

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

       A2: s <> q and

       A3: r <= 1;

      assume

       A4: r >= 1;

      

      then s = (((1 - 1) * p) + (r * q)) by A1, A3, XXREAL_0: 1

      .= (( 0 * p) + (1 * q)) by A3, A4, XXREAL_0: 1

      .= (( 0. ( TOP-REAL 2)) + (1 * q)) by RLVECT_1: 10

      .= (1 * q) by RLVECT_1: 4

      .= q by RLVECT_1:def 8;

      hence thesis by A2;

    end;

    theorem :: TOPREAL6:29

    s in ( LSeg (p,q)) & s <> p & s <> q & (p `1 ) < (q `1 ) implies (p `1 ) < (s `1 ) & (s `1 ) < (q `1 )

    proof

      assume that

       A1: s in ( LSeg (p,q)) and

       A2: s <> p and

       A3: s <> q and

       A4: (p `1 ) < (q `1 );

      

       A5: ((p `1 ) - (q `1 )) < 0 by A4, XREAL_1: 49;

      consider r such that

       A6: s = (((1 - r) * p) + (r * q)) and

       A7: 0 <= r and

       A8: r <= 1 by A1;

      ((1 - r) * p) = |[((1 - r) * (p `1 )), ((1 - r) * (p `2 ))]| by Th24;

      then

       A9: (((1 - r) * p) `1 ) = ((1 - r) * (p `1 )) by EUCLID: 52;

      (r * q) = |[(r * (q `1 )), (r * (q `2 ))]| by Th24;

      then

       A10: ((r * q) `1 ) = (r * (q `1 )) by EUCLID: 52;

      s = |[((((1 - r) * p) `1 ) + ((r * q) `1 )), ((((1 - r) * p) `2 ) + ((r * q) `2 ))]| by A6, EUCLID: 55;

      then

       A11: (s `1 ) = (((1 - r) * (p `1 )) + (r * (q `1 ))) by A9, A10, EUCLID: 52;

      then

       A12: ((p `1 ) - (s `1 )) = (r * ((p `1 ) - (q `1 )));

      r < 1 by A3, A6, A8, Th26;

      then

       A13: (1 - r) > 0 by XREAL_1: 50;

      

       A14: ((q `1 ) - (p `1 )) > 0 by A4, XREAL_1: 50;

      r > 0 by A2, A6, A7, Th25;

      then

       A15: ((p `1 ) - (s `1 )) < 0 by A12, A5, XREAL_1: 132;

      ((q `1 ) - (s `1 )) = ((1 - r) * ((q `1 ) - (p `1 ))) by A11;

      then ((q `1 ) - (s `1 )) > 0 by A14, A13, XREAL_1: 129;

      hence thesis by A15, XREAL_1: 47, XREAL_1: 48;

    end;

    theorem :: TOPREAL6:30

    s in ( LSeg (p,q)) & s <> p & s <> q & (p `2 ) < (q `2 ) implies (p `2 ) < (s `2 ) & (s `2 ) < (q `2 )

    proof

      assume that

       A1: s in ( LSeg (p,q)) and

       A2: s <> p and

       A3: s <> q and

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

      

       A5: ((p `2 ) - (q `2 )) < 0 by A4, XREAL_1: 49;

      consider r such that

       A6: s = (((1 - r) * p) + (r * q)) and

       A7: 0 <= r and

       A8: r <= 1 by A1;

      ((1 - r) * p) = |[((1 - r) * (p `1 )), ((1 - r) * (p `2 ))]| by Th24;

      then

       A9: (((1 - r) * p) `2 ) = ((1 - r) * (p `2 )) by EUCLID: 52;

      (r * q) = |[(r * (q `1 )), (r * (q `2 ))]| by Th24;

      then

       A10: ((r * q) `2 ) = (r * (q `2 )) by EUCLID: 52;

      s = |[((((1 - r) * p) `1 ) + ((r * q) `1 )), ((((1 - r) * p) `2 ) + ((r * q) `2 ))]| by A6, EUCLID: 55;

      then

       A11: (s `2 ) = (((1 - r) * (p `2 )) + (r * (q `2 ))) by A9, A10, EUCLID: 52;

      then

       A12: ((p `2 ) - (s `2 )) = (r * ((p `2 ) - (q `2 )));

      r < 1 by A3, A6, A8, Th26;

      then

       A13: (1 - r) > 0 by XREAL_1: 50;

      

       A14: ((q `2 ) - (p `2 )) > 0 by A4, XREAL_1: 50;

      r > 0 by A2, A6, A7, Th25;

      then

       A15: ((p `2 ) - (s `2 )) < 0 by A12, A5, XREAL_1: 132;

      ((q `2 ) - (s `2 )) = ((1 - r) * ((q `2 ) - (p `2 ))) by A11;

      then ((q `2 ) - (s `2 )) > 0 by A14, A13, XREAL_1: 129;

      hence thesis by A15, XREAL_1: 47, XREAL_1: 48;

    end;

    theorem :: TOPREAL6:31

    for p be Point of ( TOP-REAL 2) holds ex q be Point of ( TOP-REAL 2) st (q `1 ) < ( W-bound D) & p <> q

    proof

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

      take q = |[(( W-bound D) - 1), ((p `2 ) - 1)]|;

      (( W-bound D) - 1) < (( W-bound D) - 0 ) by XREAL_1: 15;

      hence (q `1 ) < ( W-bound D) by EUCLID: 52;

      ((p `2 ) - 1) < ((p `2 ) - 0 ) by XREAL_1: 15;

      hence thesis by EUCLID: 52;

    end;

    theorem :: TOPREAL6:32

    for p be Point of ( TOP-REAL 2) holds ex q be Point of ( TOP-REAL 2) st (q `1 ) > ( E-bound D) & p <> q

    proof

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

      take q = |[(( E-bound D) + 1), ((p `2 ) - 1)]|;

      (( E-bound D) + 1) > (( E-bound D) + 0 ) by XREAL_1: 6;

      hence (q `1 ) > ( E-bound D) by EUCLID: 52;

      ((p `2 ) - 1) < ((p `2 ) - 0 ) by XREAL_1: 15;

      hence thesis by EUCLID: 52;

    end;

    theorem :: TOPREAL6:33

    for p be Point of ( TOP-REAL 2) holds ex q be Point of ( TOP-REAL 2) st (q `2 ) > ( N-bound D) & p <> q

    proof

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

      take q = |[((p `1 ) - 1), (( N-bound D) + 1)]|;

      (( N-bound D) + 1) > (( N-bound D) + 0 ) by XREAL_1: 6;

      hence (q `2 ) > ( N-bound D) by EUCLID: 52;

      ((p `1 ) - 1) < ((p `1 ) - 0 ) by XREAL_1: 15;

      hence thesis by EUCLID: 52;

    end;

    theorem :: TOPREAL6:34

    for p be Point of ( TOP-REAL 2) holds ex q be Point of ( TOP-REAL 2) st (q `2 ) < ( S-bound D) & p <> q

    proof

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

      take q = |[((p `1 ) - 1), (( S-bound D) - 1)]|;

      (( S-bound D) - 1) < (( S-bound D) - 0 ) by XREAL_1: 15;

      hence (q `2 ) < ( S-bound D) by EUCLID: 52;

      ((p `1 ) - 1) < ((p `1 ) - 0 ) by XREAL_1: 15;

      hence thesis by EUCLID: 52;

    end;

    registration

      cluster non horizontal -> non empty for Subset of ( TOP-REAL 2);

      coherence ;

      cluster non vertical -> non empty for Subset of ( TOP-REAL 2);

      coherence ;

      cluster being_Region -> open connected for Subset of ( TOP-REAL 2);

      coherence by TOPREAL4:def 3;

      cluster open connected -> being_Region for Subset of ( TOP-REAL 2);

      coherence by TOPREAL4:def 3;

    end

    registration

      cluster empty -> horizontal for Subset of ( TOP-REAL 2);

      coherence ;

      cluster empty -> vertical for Subset of ( TOP-REAL 2);

      coherence ;

    end

    registration

      cluster non empty convex for Subset of ( TOP-REAL 2);

      existence

      proof

        set C = the non empty convex Subset of ( TOP-REAL 2);

        take C;

        thus thesis;

      end;

    end

    registration

      let a,b be Point of ( TOP-REAL 2);

      cluster ( LSeg (a,b)) -> connected;

      coherence ;

    end

    registration

      cluster R^2-unit_square -> connected;

      coherence

      proof

        

         A1: ( LSeg ( |[ 0 , 1]|, |[1, 1]|)) meets ( LSeg ( |[1, 0 ]|, |[1, 1]|)) by TOPREAL1: 18;

        

         A2: ( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|)) meets ( LSeg ( |[1, 0 ]|, |[1, 1]|)) by TOPREAL1: 16;

        

         A3: ( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) meets ( LSeg ( |[ 0 , 1]|, |[1, 1]|)) by TOPREAL1: 15;

         R^2-unit_square = (((( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) \/ ( LSeg ( |[ 0 , 1]|, |[1, 1]|))) \/ ( LSeg ( |[1, 1]|, |[1, 0 ]|))) \/ ( LSeg ( |[1, 0 ]|, |[ 0 , 0 ]|))) by TOPREAL1:def 2, XBOOLE_1: 4;

        hence thesis by A3, A2, A1, JORDAN1: 5;

      end;

    end

    registration

      cluster being_simple_closed_curve -> connected for Subset of ( TOP-REAL 2);

      coherence

      proof

        let P be Subset of ( TOP-REAL 2);

        given f be Function of (( TOP-REAL 2) | R^2-unit_square ), (( TOP-REAL 2) | P) such that

         A1: f is being_homeomorphism;

        

         A2: ((( TOP-REAL 2) | R^2-unit_square ),(( TOP-REAL 2) | P)) are_homeomorphic by A1;

        (( TOP-REAL 2) | R^2-unit_square ) is connected by CONNSP_1:def 3;

        then (( TOP-REAL 2) | P) is connected by A2, Th17;

        hence thesis;

      end;

    end

    theorem :: TOPREAL6:35

    ( LSeg (( NE-corner P),( SE-corner P))) c= ( L~ ( SpStSeq P))

    proof

      

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

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

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

      hence thesis by SPRECT_1: 41;

    end;

    theorem :: TOPREAL6:36

    ( LSeg (( SW-corner P),( SE-corner P))) c= ( L~ ( SpStSeq P))

    proof

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

      then

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

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

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

      hence thesis by SPRECT_1: 41;

    end;

    theorem :: TOPREAL6:37

    ( LSeg (( SW-corner P),( NW-corner P))) c= ( L~ ( SpStSeq P))

    proof

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

      then ( LSeg (( SW-corner P),( NW-corner P))) c= ((( LSeg (( NW-corner P),( NE-corner P))) \/ ( LSeg (( NE-corner P),( SE-corner P)))) \/ (( LSeg (( SE-corner P),( SW-corner P))) \/ ( LSeg (( SW-corner P),( NW-corner P))))) by XBOOLE_1: 4;

      hence thesis by SPRECT_1: 41;

    end;

    theorem :: TOPREAL6:38

    for C be Subset of ( TOP-REAL 2) holds { p where p be Point of ( TOP-REAL 2) : (p `1 ) < ( W-bound C) } is non empty convex connected Subset of ( TOP-REAL 2)

    proof

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

      set A = { p where p be Point of ( TOP-REAL 2) : (p `1 ) < ( W-bound C) };

      A c= the carrier of ( TOP-REAL 2)

      proof

        let a be object;

        assume a in A;

        then ex p be Point of ( TOP-REAL 2) st a = p & (p `1 ) < ( W-bound C);

        hence thesis;

      end;

      then

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

      set p = ( W-bound C);

      set b = |[(p - 1), 0 ]|;

      

       A1: (b `1 ) = (p - 1) by EUCLID: 52;

      (p - 1) < (p - 0 ) by XREAL_1: 15;

      then

       A2: b in A by A1;

      A is convex

      proof

        let w1,w2 be Point of ( TOP-REAL 2);

        assume w1 in A;

        then

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

         A3: w1 = p and

         A4: (p `1 ) < ( W-bound C);

        assume w2 in A;

        then

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

         A5: w2 = q and

         A6: (q `1 ) < ( W-bound C);

        let k be object;

        assume

         A7: k in ( LSeg (w1,w2));

        then

        reconsider z = k as Point of ( TOP-REAL 2);

        per cases by XXREAL_0: 1;

          suppose (p `1 ) < (q `1 );

          then (z `1 ) <= (w2 `1 ) by A3, A5, A7, TOPREAL1: 3;

          then (z `1 ) < ( W-bound C) by A5, A6, XXREAL_0: 2;

          hence thesis;

        end;

          suppose (q `1 ) < (p `1 );

          then (z `1 ) <= (w1 `1 ) by A3, A5, A7, TOPREAL1: 3;

          then (z `1 ) < ( W-bound C) by A3, A4, XXREAL_0: 2;

          hence thesis;

        end;

          suppose (p `1 ) = (q `1 );

          then (z `1 ) = (p `1 ) by A3, A5, A7, GOBOARD7: 5;

          hence thesis by A4;

        end;

      end;

      then

      reconsider A as non empty convex Subset of ( TOP-REAL 2) by A2;

      A is connected;

      hence thesis;

    end;

    begin

    reserve r for Real;

    theorem :: TOPREAL6:39

    

     Th37: e = q & p in ( Ball (e,r)) implies ((q `1 ) - r) < (p `1 ) & (p `1 ) < ((q `1 ) + r)

    proof

      assume that

       A1: e = q and

       A2: p in ( Ball (e,r));

      reconsider f = p as Point of ( Euclid 2) by TOPREAL3: 8;

      

       A3: ( dist (e,f)) < r by A2, METRIC_1: 11;

      

       A4: ( dist (e,f)) = (( Pitag_dist 2) . (e,f)) by METRIC_1:def 1

      .= ( sqrt ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 ))) by A1, TOPREAL3: 7;

      

       A5: r > 0 by A2, TBSP_1: 12;

      assume

       A6: not thesis;

      per cases by A6;

        suppose

         A7: ((q `1 ) - r) >= (p `1 );

        (((q `2 ) - (p `2 )) ^2 ) >= 0 by XREAL_1: 63;

        then

         A8: ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 )) >= ((((q `1 ) - (p `1 )) ^2 ) + 0 ) by XREAL_1: 6;

        ((q `1 ) - (p `1 )) >= r by A7, XREAL_1: 11;

        then (((q `1 ) - (p `1 )) ^2 ) >= (r ^2 ) by A5, SQUARE_1: 15;

        then ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 )) >= (r ^2 ) by A8, XXREAL_0: 2;

        then ( sqrt ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 ))) >= ( sqrt (r ^2 )) by A5, SQUARE_1: 26;

        hence contradiction by A3, A4, A5, SQUARE_1: 22;

      end;

        suppose

         A9: (p `1 ) >= ((q `1 ) + r);

        (((q `2 ) - (p `2 )) ^2 ) >= 0 by XREAL_1: 63;

        then

         A10: ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 )) >= ((((q `1 ) - (p `1 )) ^2 ) + 0 ) by XREAL_1: 6;

        ((p `1 ) - (q `1 )) >= r by A9, XREAL_1: 19;

        then (( - ((q `1 ) - (p `1 ))) ^2 ) >= (r ^2 ) by A5, SQUARE_1: 15;

        then ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 )) >= (r ^2 ) by A10, XXREAL_0: 2;

        then ( sqrt ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 ))) >= ( sqrt (r ^2 )) by A5, SQUARE_1: 26;

        hence contradiction by A3, A4, A5, SQUARE_1: 22;

      end;

    end;

    theorem :: TOPREAL6:40

    

     Th38: e = q & p in ( Ball (e,r)) implies ((q `2 ) - r) < (p `2 ) & (p `2 ) < ((q `2 ) + r)

    proof

      assume that

       A1: e = q and

       A2: p in ( Ball (e,r));

      reconsider f = p as Point of ( Euclid 2) by TOPREAL3: 8;

      

       A3: ( dist (e,f)) < r by A2, METRIC_1: 11;

      

       A4: ( dist (e,f)) = (( Pitag_dist 2) . (e,f)) by METRIC_1:def 1

      .= ( sqrt ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 ))) by A1, TOPREAL3: 7;

      

       A5: r > 0 by A2, TBSP_1: 12;

      assume

       A6: not thesis;

      per cases by A6;

        suppose

         A7: ((q `2 ) - r) >= (p `2 );

        (((q `1 ) - (p `1 )) ^2 ) >= 0 by XREAL_1: 63;

        then

         A8: ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 )) >= ((((q `2 ) - (p `2 )) ^2 ) + 0 ) by XREAL_1: 6;

        ((q `2 ) - (p `2 )) >= r by A7, XREAL_1: 11;

        then (((q `2 ) - (p `2 )) ^2 ) >= (r ^2 ) by A5, SQUARE_1: 15;

        then ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 )) >= (r ^2 ) by A8, XXREAL_0: 2;

        then ( sqrt ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 ))) >= ( sqrt (r ^2 )) by A5, SQUARE_1: 26;

        hence contradiction by A3, A4, A5, SQUARE_1: 22;

      end;

        suppose

         A9: (p `2 ) >= ((q `2 ) + r);

        (((q `1 ) - (p `1 )) ^2 ) >= 0 by XREAL_1: 63;

        then

         A10: ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 )) >= ((((q `2 ) - (p `2 )) ^2 ) + 0 ) by XREAL_1: 6;

        ((p `2 ) - (q `2 )) >= r by A9, XREAL_1: 19;

        then (( - ((q `2 ) - (p `2 ))) ^2 ) >= (r ^2 ) by A5, SQUARE_1: 15;

        then ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 )) >= (r ^2 ) by A10, XXREAL_0: 2;

        then ( sqrt ((((q `1 ) - (p `1 )) ^2 ) + (((q `2 ) - (p `2 )) ^2 ))) >= ( sqrt (r ^2 )) by A5, SQUARE_1: 26;

        hence contradiction by A3, A4, A5, SQUARE_1: 22;

      end;

    end;

    theorem :: TOPREAL6:41

    

     Th39: p = e implies ( product ((1,2) --> ( ].((p `1 ) - (r / ( sqrt 2))), ((p `1 ) + (r / ( sqrt 2))).[, ].((p `2 ) - (r / ( sqrt 2))), ((p `2 ) + (r / ( sqrt 2))).[))) c= ( Ball (e,r))

    proof

      set A = ].((p `1 ) - (r / ( sqrt 2))), ((p `1 ) + (r / ( sqrt 2))).[, B = ].((p `2 ) - (r / ( sqrt 2))), ((p `2 ) + (r / ( sqrt 2))).[, f = ((1,2) --> (A,B));

      assume

       A1: p = e;

      let a be object;

      

       A2: A = { m where m be Real : ((p `1 ) - (r / ( sqrt 2))) < m & m < ((p `1 ) + (r / ( sqrt 2))) } by RCOMP_1:def 2;

      

       A3: (f . 2) = B by FUNCT_4: 63;

      

       A4: B = { n where n be Real : ((p `2 ) - (r / ( sqrt 2))) < n & n < ((p `2 ) + (r / ( sqrt 2))) } by RCOMP_1:def 2;

      

       A5: (f . 1) = A by FUNCT_4: 63;

      assume a in ( product f);

      then

      consider g be Function such that

       A6: a = g and

       A7: ( dom g) = ( dom f) and

       A8: for x be object st x in ( dom f) holds (g . x) in (f . x) by CARD_3:def 5;

      

       A9: ( dom f) = {1, 2} by FUNCT_4: 62;

      then 1 in ( dom f) by TARSKI:def 2;

      then

       A10: (g . 1) in A by A8, A5;

      then

      consider m be Real such that

       A11: m = (g . 1) and ((p `1 ) - (r / ( sqrt 2))) < m and m < ((p `1 ) + (r / ( sqrt 2))) by A2;

      

       A12: 0 <= ((m - (p `1 )) ^2 ) by XREAL_1: 63;

      2 in ( dom f) by A9, TARSKI:def 2;

      then

       A13: (g . 2) in B by A8, A3;

      then

      consider n be Real such that

       A14: n = (g . 2) and ((p `2 ) - (r / ( sqrt 2))) < n and n < ((p `2 ) + (r / ( sqrt 2))) by A4;

       |.(n - (p `2 )).| < (r / ( sqrt 2)) by A13, A14, RCOMP_1: 1;

      then ( |.(n - (p `2 )).| ^2 ) < ((r / ( sqrt 2)) ^2 ) by COMPLEX1: 46, SQUARE_1: 16;

      then ( |.(n - (p `2 )).| ^2 ) < ((r ^2 ) / (( sqrt 2) ^2 )) by XCMPLX_1: 76;

      then ( |.(n - (p `2 )).| ^2 ) < ((r ^2 ) / 2) by SQUARE_1:def 2;

      then

       A15: ((n - (p `2 )) ^2 ) < ((r ^2 ) / 2) by COMPLEX1: 75;

      ((p `1 ) - ((p `1 ) + (r / ( sqrt 2)))) < ((p `1 ) - ((p `1 ) - (r / ( sqrt 2)))) by A10, XREAL_1: 15, XXREAL_1: 28;

      then (( - (r / ( sqrt 2))) + (r / ( sqrt 2))) < ((r / ( sqrt 2)) + (r / ( sqrt 2))) by XREAL_1: 6;

      then

       A16: 0 < r by SQUARE_1: 19;

       A17:

      now

        let k be object;

        assume k in ( dom g);

        then k = 1 or k = 2 by A7, TARSKI:def 2;

        hence (g . k) = ( <*(g . 1), (g . 2)*> . k) by FINSEQ_1: 44;

      end;

      

       A18: 0 <= ((n - (p `2 )) ^2 ) by XREAL_1: 63;

       |.(m - (p `1 )).| < (r / ( sqrt 2)) by A10, A11, RCOMP_1: 1;

      then ( |.(m - (p `1 )).| ^2 ) < ((r / ( sqrt 2)) ^2 ) by COMPLEX1: 46, SQUARE_1: 16;

      then ( |.(m - (p `1 )).| ^2 ) < ((r ^2 ) / (( sqrt 2) ^2 )) by XCMPLX_1: 76;

      then ( |.(m - (p `1 )).| ^2 ) < ((r ^2 ) / 2) by SQUARE_1:def 2;

      then ((m - (p `1 )) ^2 ) < ((r ^2 ) / 2) by COMPLEX1: 75;

      then (((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 )) < (((r ^2 ) / 2) + ((r ^2 ) / 2)) by A15, XREAL_1: 8;

      then ( sqrt (((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 ))) < ( sqrt (r ^2 )) by A12, A18, SQUARE_1: 27;

      then

       A19: ( sqrt (((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 ))) < r by A16, SQUARE_1: 22;

      ( dom <*(g . 1), (g . 2)*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      then a = |[m, n]| by A6, A7, A11, A14, A17, FUNCT_1: 2, FUNCT_4: 62;

      then

      reconsider c = a as Point of ( TOP-REAL 2);

      reconsider b = c as Point of ( Euclid 2) by TOPREAL3: 8;

      ( dist (b,e)) = (( Pitag_dist 2) . (b,e)) by METRIC_1:def 1

      .= ( sqrt ((((c `1 ) - (p `1 )) ^2 ) + (((c `2 ) - (p `2 )) ^2 ))) by A1, TOPREAL3: 7;

      hence thesis by A6, A11, A14, A19, METRIC_1: 11;

    end;

    theorem :: TOPREAL6:42

    

     Th40: p = e implies ( Ball (e,r)) c= ( product ((1,2) --> ( ].((p `1 ) - r), ((p `1 ) + r).[, ].((p `2 ) - r), ((p `2 ) + r).[)))

    proof

      set A = ].((p `1 ) - r), ((p `1 ) + r).[, B = ].((p `2 ) - r), ((p `2 ) + r).[, f = ((1,2) --> (A,B));

      assume that

       A1: p = e;

      let a be object;

      assume

       A2: a in ( Ball (e,r));

      then

      reconsider b = a as Point of ( Euclid 2);

      reconsider q = b as Point of ( TOP-REAL 2) by TOPREAL3: 8;

      reconsider g = q as FinSequence;

      

       A3: for x be object st x in ( dom f) holds (g . x) in (f . x)

      proof

        let x be object;

        assume

         A4: x in ( dom f);

        per cases by A4, TARSKI:def 2;

          suppose

           A5: x = 1;

          

           A6: (f . 1) = A by FUNCT_4: 63;

          

           A7: (q `1 ) < ((p `1 ) + r) by A1, A2, Th37;

          ((p `1 ) - r) < (q `1 ) by A1, A2, Th37;

          hence thesis by A5, A6, A7, XXREAL_1: 4;

        end;

          suppose

           A8: x = 2;

          

           A9: (f . 2) = B by FUNCT_4: 63;

          

           A10: (q `2 ) < ((p `2 ) + r) by A1, A2, Th38;

          ((p `2 ) - r) < (q `2 ) by A1, A2, Th38;

          hence thesis by A8, A9, A10, XXREAL_1: 4;

        end;

      end;

      q is Function of ( Seg 2), REAL by EUCLID: 23;

      then

       A11: ( dom g) = {1, 2} by FINSEQ_1: 2, FUNCT_2:def 1;

      ( dom f) = {1, 2} by FUNCT_4: 62;

      hence thesis by A11, A3, CARD_3: 9;

    end;

    theorem :: TOPREAL6:43

    

     Th41: P = ( Ball (e,r)) & p = e implies ( proj1 .: P) = ].((p `1 ) - r), ((p `1 ) + r).[

    proof

      assume that

       A1: P = ( Ball (e,r)) and

       A2: p = e;

      hereby

        let a be object;

        assume a in ( proj1 .: P);

        then

        consider x be object such that

         A3: x in the carrier of ( TOP-REAL 2) and

         A4: x in P and

         A5: a = ( proj1 . x) by FUNCT_2: 64;

        reconsider b = a as Real by A5;

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

        

         A6: a = (x `1 ) by A5, PSCOMP_1:def 5;

        then

         A7: b < ((p `1 ) + r) by A1, A2, A4, Th37;

        ((p `1 ) - r) < b by A1, A2, A4, A6, Th37;

        hence a in ].((p `1 ) - r), ((p `1 ) + r).[ by A7, XXREAL_1: 4;

      end;

      let a be object;

      assume

       A8: a in ].((p `1 ) - r), ((p `1 ) + r).[;

      then

      reconsider b = a as Real;

      reconsider f = |[b, (p `2 )]| as Point of ( Euclid 2) by TOPREAL3: 8;

      

       A9: ( dist (f,e)) = (( Pitag_dist 2) . (f,e)) by METRIC_1:def 1

      .= ( sqrt (((( |[b, (p `2 )]| `1 ) - (p `1 )) ^2 ) + ((( |[b, (p `2 )]| `2 ) - (p `2 )) ^2 ))) by A2, TOPREAL3: 7

      .= ( sqrt (((b - (p `1 )) ^2 ) + ((( |[b, (p `2 )]| `2 ) - (p `2 )) ^2 ))) by EUCLID: 52

      .= ( sqrt (((b - (p `1 )) ^2 ) + (((p `2 ) - (p `2 )) ^2 ))) by EUCLID: 52

      .= ( sqrt (((b - (p `1 )) ^2 ) + 0 ));

      b < ((p `1 ) + r) by A8, XXREAL_1: 4;

      then

       A10: (b - (p `1 )) < (((p `1 ) + r) - (p `1 )) by XREAL_1: 9;

      now

        per cases ;

          case 0 <= (b - (p `1 ));

          hence ( dist (f,e)) < r by A10, A9, SQUARE_1: 22;

        end;

          case

           A11: 0 > (b - (p `1 ));

          ((p `1 ) - r) < b by A8, XXREAL_1: 4;

          then (((p `1 ) - r) + r) < (b + r) by XREAL_1: 6;

          then

           A12: ((p `1 ) - b) < ((r + b) - b) by XREAL_1: 9;

          ( sqrt ((b - (p `1 )) ^2 )) = ( sqrt (( - (b - (p `1 ))) ^2 ))

          .= ( - (b - (p `1 ))) by A11, SQUARE_1: 22;

          hence ( dist (f,e)) < r by A9, A12;

        end;

      end;

      then

       A13: |[b, (p `2 )]| in P by A1, METRIC_1: 11;

      a = ( |[b, (p `2 )]| `1 ) by EUCLID: 52

      .= ( proj1 . |[b, (p `2 )]|) by PSCOMP_1:def 5;

      hence thesis by A13, FUNCT_2: 35;

    end;

    theorem :: TOPREAL6:44

    

     Th42: P = ( Ball (e,r)) & p = e implies ( proj2 .: P) = ].((p `2 ) - r), ((p `2 ) + r).[

    proof

      assume that

       A1: P = ( Ball (e,r)) and

       A2: p = e;

      hereby

        let a be object;

        assume a in ( proj2 .: P);

        then

        consider x be object such that

         A3: x in the carrier of ( TOP-REAL 2) and

         A4: x in P and

         A5: a = ( proj2 . x) by FUNCT_2: 64;

        reconsider b = a as Real by A5;

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

        

         A6: a = (x `2 ) by A5, PSCOMP_1:def 6;

        then

         A7: b < ((p `2 ) + r) by A1, A2, A4, Th38;

        ((p `2 ) - r) < b by A1, A2, A4, A6, Th38;

        hence a in ].((p `2 ) - r), ((p `2 ) + r).[ by A7, XXREAL_1: 4;

      end;

      let a be object;

      assume

       A8: a in ].((p `2 ) - r), ((p `2 ) + r).[;

      then

      reconsider b = a as Real;

      reconsider f = |[(p `1 ), b]| as Point of ( Euclid 2) by TOPREAL3: 8;

      

       A9: ( dist (f,e)) = (( Pitag_dist 2) . (f,e)) by METRIC_1:def 1

      .= ( sqrt (((( |[(p `1 ), b]| `1 ) - (p `1 )) ^2 ) + ((( |[(p `1 ), b]| `2 ) - (p `2 )) ^2 ))) by A2, TOPREAL3: 7

      .= ( sqrt ((((p `1 ) - (p `1 )) ^2 ) + ((( |[(p `1 ), b]| `2 ) - (p `2 )) ^2 ))) by EUCLID: 52

      .= ( sqrt ( 0 + ((b - (p `2 )) ^2 ))) by EUCLID: 52;

      b < ((p `2 ) + r) by A8, XXREAL_1: 4;

      then

       A10: (b - (p `2 )) < (((p `2 ) + r) - (p `2 )) by XREAL_1: 9;

      now

        per cases ;

          case 0 <= (b - (p `2 ));

          hence ( dist (f,e)) < r by A10, A9, SQUARE_1: 22;

        end;

          case

           A11: 0 > (b - (p `2 ));

          ((p `2 ) - r) < b by A8, XXREAL_1: 4;

          then (((p `2 ) - r) + r) < (b + r) by XREAL_1: 6;

          then

           A12: ((p `2 ) - b) < ((r + b) - b) by XREAL_1: 9;

          ( sqrt ((b - (p `2 )) ^2 )) = ( sqrt (( - (b - (p `2 ))) ^2 ))

          .= ( - (b - (p `2 ))) by A11, SQUARE_1: 22;

          hence ( dist (f,e)) < r by A9, A12;

        end;

      end;

      then

       A13: |[(p `1 ), b]| in P by A1, METRIC_1: 11;

      a = ( |[(p `1 ), b]| `2 ) by EUCLID: 52

      .= ( proj2 . |[(p `1 ), b]|) by PSCOMP_1:def 6;

      hence thesis by A13, FUNCT_2: 35;

    end;

    theorem :: TOPREAL6:45

    D = ( Ball (e,r)) & p = e implies ( W-bound D) = ((p `1 ) - r)

    proof

      assume that

       A1: D = ( Ball (e,r)) and

       A2: p = e;

      r > 0 by A1, TBSP_1: 12;

      then

       A3: ((p `1 ) + 0 ) < ((p `1 ) + r) by XREAL_1: 6;

      ((p `1 ) - r) < ((p `1 ) - 0 ) by A1, TBSP_1: 12, XREAL_1: 15;

      then ((p `1 ) - r) < ((p `1 ) + r) by A3, XXREAL_0: 2;

      then

       A4: ( lower_bound ].((p `1 ) - r), ((p `1 ) + r).[) = ((p `1 ) - r) by Th16;

      ( proj1 .: D) = ].((p `1 ) - r), ((p `1 ) + r).[ by A1, A2, Th41;

      hence thesis by A4, SPRECT_1: 43;

    end;

    theorem :: TOPREAL6:46

    D = ( Ball (e,r)) & p = e implies ( E-bound D) = ((p `1 ) + r)

    proof

      assume that

       A1: D = ( Ball (e,r)) and

       A2: p = e;

      r > 0 by A1, TBSP_1: 12;

      then

       A3: ((p `1 ) + 0 ) < ((p `1 ) + r) by XREAL_1: 6;

      ((p `1 ) - r) < ((p `1 ) - 0 ) by A1, TBSP_1: 12, XREAL_1: 15;

      then ((p `1 ) - r) < ((p `1 ) + r) by A3, XXREAL_0: 2;

      then

       A4: ( upper_bound ].((p `1 ) - r), ((p `1 ) + r).[) = ((p `1 ) + r) by Th16;

      ( proj1 .: D) = ].((p `1 ) - r), ((p `1 ) + r).[ by A1, A2, Th41;

      hence thesis by A4, SPRECT_1: 46;

    end;

    theorem :: TOPREAL6:47

    D = ( Ball (e,r)) & p = e implies ( S-bound D) = ((p `2 ) - r)

    proof

      assume that

       A1: D = ( Ball (e,r)) and

       A2: p = e;

      r > 0 by A1, TBSP_1: 12;

      then

       A3: ((p `2 ) + 0 ) < ((p `2 ) + r) by XREAL_1: 6;

      ((p `2 ) - r) < ((p `2 ) - 0 ) by A1, TBSP_1: 12, XREAL_1: 15;

      then ((p `2 ) - r) < ((p `2 ) + r) by A3, XXREAL_0: 2;

      then

       A4: ( lower_bound ].((p `2 ) - r), ((p `2 ) + r).[) = ((p `2 ) - r) by Th16;

      ( proj2 .: D) = ].((p `2 ) - r), ((p `2 ) + r).[ by A1, A2, Th42;

      hence thesis by A4, SPRECT_1: 44;

    end;

    theorem :: TOPREAL6:48

    D = ( Ball (e,r)) & p = e implies ( N-bound D) = ((p `2 ) + r)

    proof

      assume that

       A1: D = ( Ball (e,r)) and

       A2: p = e;

      r > 0 by A1, TBSP_1: 12;

      then

       A3: ((p `2 ) + 0 ) < ((p `2 ) + r) by XREAL_1: 6;

      ((p `2 ) - r) < ((p `2 ) - 0 ) by A1, TBSP_1: 12, XREAL_1: 15;

      then ((p `2 ) - r) < ((p `2 ) + r) by A3, XXREAL_0: 2;

      then

       A4: ( upper_bound ].((p `2 ) - r), ((p `2 ) + r).[) = ((p `2 ) + r) by Th16;

      ( proj2 .: D) = ].((p `2 ) - r), ((p `2 ) + r).[ by A1, A2, Th42;

      hence thesis by A4, SPRECT_1: 45;

    end;

    theorem :: TOPREAL6:49

    D = ( Ball (e,r)) implies D is non horizontal

    proof

      reconsider p = e as Point of ( TOP-REAL 2) by TOPREAL3: 8;

      assume

       A1: D = ( Ball (e,r));

      then

       A2: r > 0 by TBSP_1: 12;

      take p, q = |[(p `1 ), ((p `2 ) - (r / 2))]|;

      thus p in D by A1, TBSP_1: 11, TBSP_1: 12;

      reconsider f = q as Point of ( Euclid 2) by TOPREAL3: 8;

      ( dist (e,f)) = (( Pitag_dist 2) . (e,f)) by METRIC_1:def 1

      .= ( sqrt ((((p `1 ) - (q `1 )) ^2 ) + (((p `2 ) - (q `2 )) ^2 ))) by TOPREAL3: 7

      .= ( sqrt ((((p `1 ) - (p `1 )) ^2 ) + (((p `2 ) - (q `2 )) ^2 ))) by EUCLID: 52

      .= ( sqrt ( 0 + (((p `2 ) - ((p `2 ) - (r / 2))) ^2 ))) by EUCLID: 52

      .= (r / 2) by A2, SQUARE_1: 22;

      then ( dist (e,f)) < r by A1, TBSP_1: 12, XREAL_1: 216;

      hence q in D by A1, METRIC_1: 11;

      (r / 2) > 0 by A2, XREAL_1: 139;

      then ((p `2 ) - (r / 2)) < ((p `2 ) - 0 ) by XREAL_1: 15;

      hence thesis by EUCLID: 52;

    end;

    theorem :: TOPREAL6:50

    D = ( Ball (e,r)) implies D is non vertical

    proof

      reconsider p = e as Point of ( TOP-REAL 2) by TOPREAL3: 8;

      assume

       A1: D = ( Ball (e,r));

      then

       A2: r > 0 by TBSP_1: 12;

      take p, q = |[((p `1 ) - (r / 2)), (p `2 )]|;

      thus p in D by A1, TBSP_1: 11, TBSP_1: 12;

      reconsider f = q as Point of ( Euclid 2) by TOPREAL3: 8;

      ( dist (e,f)) = (( Pitag_dist 2) . (e,f)) by METRIC_1:def 1

      .= ( sqrt ((((p `1 ) - (q `1 )) ^2 ) + (((p `2 ) - (q `2 )) ^2 ))) by TOPREAL3: 7

      .= ( sqrt ((((p `1 ) - ((p `1 ) - (r / 2))) ^2 ) + (((p `2 ) - (q `2 )) ^2 ))) by EUCLID: 52

      .= ( sqrt ((((p `1 ) - ((p `1 ) - (r / 2))) ^2 ) + (((p `2 ) - (p `2 )) ^2 ))) by EUCLID: 52

      .= (r / 2) by A2, SQUARE_1: 22;

      then ( dist (e,f)) < r by A1, TBSP_1: 12, XREAL_1: 216;

      hence q in D by A1, METRIC_1: 11;

      (r / 2) > 0 by A2, XREAL_1: 139;

      then ((p `1 ) - (r / 2)) < ((p `1 ) - 0 ) by XREAL_1: 15;

      hence thesis by EUCLID: 52;

    end;

    theorem :: TOPREAL6:51

    for f be Point of ( Euclid 2), x be Point of ( TOP-REAL 2) st x in ( Ball (f,a)) holds not |[((x `1 ) - (2 * a)), (x `2 )]| in ( Ball (f,a))

    proof

      let f be Point of ( Euclid 2), x be Point of ( TOP-REAL 2) such that

       A1: x in ( Ball (f,a));

      

       A2: a > 0 by A1, TBSP_1: 12;

      set p = |[((x `1 ) - (2 * a)), (x `2 )]|;

      reconsider z = p, X = x as Point of ( Euclid 2) by TOPREAL3: 8;

      

       A3: ( dist (X,z)) = (( Pitag_dist 2) . (X,z)) by METRIC_1:def 1

      .= ( sqrt ((((x `1 ) - (p `1 )) ^2 ) + (((x `2 ) - (p `2 )) ^2 ))) by TOPREAL3: 7

      .= ( sqrt ((((x `1 ) - ((x `1 ) - (2 * a))) ^2 ) + (((x `2 ) - (p `2 )) ^2 ))) by EUCLID: 52

      .= ( sqrt (((( 0 ^2 ) + ((2 * ((x `1 ) - (x `1 ))) * (2 * a))) + ((2 * a) ^2 )) + (((x `2 ) - (x `2 )) ^2 ))) by EUCLID: 52

      .= (2 * a) by A2, SQUARE_1: 22;

      assume |[((x `1 ) - (2 * a)), (x `2 )]| in ( Ball (f,a));

      then

       A4: ( dist (f,z)) < a by METRIC_1: 11;

      ( dist (f,X)) < a by A1, METRIC_1: 11;

      then (( dist (f,X)) + ( dist (f,z))) < (a + a) by A4, XREAL_1: 8;

      hence contradiction by A3, METRIC_1: 4;

    end;

    theorem :: TOPREAL6:52

    for X be non empty compact Subset of ( TOP-REAL 2), p be Point of ( Euclid 2) st p = ( 0. ( TOP-REAL 2)) & a > 0 holds X c= ( Ball (p,(((( |.( E-bound X).| + |.( N-bound X).|) + |.( W-bound X).|) + |.( S-bound X).|) + a)))

    proof

      let X be non empty compact Subset of ( TOP-REAL 2), p be Point of ( Euclid 2) such that

       A1: p = ( 0. ( TOP-REAL 2)) and

       A2: a > 0 ;

      set A = X, n = ( N-bound A), s = ( S-bound A), e = ( E-bound A), w = ( W-bound A), r = (((( |.e.| + |.n.|) + |.w.|) + |.s.|) + a);

      

       A3: (((( |.e.| + |.n.|) + |.w.|) + |.s.|) + 0 ) < (((( |.e.| + |.n.|) + |.w.|) + |.s.|) + a) by A2, XREAL_1: 8;

      let x be object;

      assume

       A4: x in X;

      then

      reconsider b = x as Point of ( Euclid 2) by TOPREAL3: 8;

      reconsider P = p, B = b as Point of ( TOP-REAL 2) by TOPREAL3: 8;

      

       A5: (P `1 ) = 0 by A1, Th22;

      

       A6: (B `1 ) <= e by A4, PSCOMP_1: 24;

      

       A7: (B `2 ) <= n by A4, PSCOMP_1: 24;

      

       A8: s <= (B `2 ) by A4, PSCOMP_1: 24;

      

       A9: (P `2 ) = 0 by A1, Th22;

      

       A10: ( dist (p,b)) = (( Pitag_dist 2) . (p,b)) by METRIC_1:def 1

      .= ( sqrt ((((P `1 ) - (B `1 )) ^2 ) + (((P `2 ) - (B `2 )) ^2 ))) by TOPREAL3: 7

      .= ( sqrt (((B `1 ) ^2 ) + ((B `2 ) ^2 ))) by A5, A9;

      

       A11: 0 <= ((B `2 ) ^2 ) by XREAL_1: 63;

       0 <= ((B `1 ) ^2 ) by XREAL_1: 63;

      then ( sqrt (((B `1 ) ^2 ) + ((B `2 ) ^2 ))) <= (( sqrt ((B `1 ) ^2 )) + ( sqrt ((B `2 ) ^2 ))) by A11, SQUARE_1: 59;

      then ( sqrt (((B `1 ) ^2 ) + ((B `2 ) ^2 ))) <= ( |.(B `1 ).| + ( sqrt ((B `2 ) ^2 ))) by COMPLEX1: 72;

      then

       A12: ( sqrt (((B `1 ) ^2 ) + ((B `2 ) ^2 ))) <= ( |.(B `1 ).| + |.(B `2 ).|) by COMPLEX1: 72;

      

       A13: 0 <= |.n.| by COMPLEX1: 46;

      

       A14: 0 <= |.e.| by COMPLEX1: 46;

      

       A15: 0 <= |.w.| by COMPLEX1: 46;

      

       A16: 0 <= |.s.| by COMPLEX1: 46;

      

       A17: w <= (B `1 ) by A4, PSCOMP_1: 24;

      now

        per cases ;

          case

           A18: (B `1 ) >= 0 & (B `2 ) >= 0 ;

          (( |.e.| + |.n.|) + 0 ) <= (( |.e.| + |.n.|) + |.w.|) by A15, XREAL_1: 7;

          then ( |.e.| + |.n.|) <= ((( |.e.| + |.n.|) + |.w.|) + |.s.|) by A16, XREAL_1: 7;

          then

           A19: ( |.e.| + |.n.|) < r by A3, XXREAL_0: 2;

          

           A20: |.(B `2 ).| <= |.n.| by A7, A18, Th1;

           |.(B `1 ).| <= |.e.| by A6, A18, Th1;

          then ( |.(B `1 ).| + |.(B `2 ).|) <= ( |.e.| + |.n.|) by A20, XREAL_1: 7;

          then ( dist (p,b)) <= ( |.e.| + |.n.|) by A10, A12, XXREAL_0: 2;

          hence ( dist (p,b)) < r by A19, XXREAL_0: 2;

        end;

          case

           A21: (B `1 ) < 0 & (B `2 ) >= 0 ;

          ( 0 + ( |.n.| + |.w.|)) <= ( |.e.| + ( |.n.| + |.w.|)) by A14, XREAL_1: 7;

          then ( |.w.| + |.n.|) <= ((( |.e.| + |.n.|) + |.w.|) + |.s.|) by A16, XREAL_1: 7;

          then

           A22: ( |.w.| + |.n.|) < r by A3, XXREAL_0: 2;

          

           A23: |.(B `2 ).| <= |.n.| by A7, A21, Th1;

           |.(B `1 ).| <= |.w.| by A17, A21, Th2;

          then ( |.(B `1 ).| + |.(B `2 ).|) <= ( |.w.| + |.n.|) by A23, XREAL_1: 7;

          then ( dist (p,b)) <= ( |.w.| + |.n.|) by A10, A12, XXREAL_0: 2;

          hence ( dist (p,b)) < r by A22, XXREAL_0: 2;

        end;

          case

           A24: (B `1 ) >= 0 & (B `2 ) < 0 ;

          

           A25: ((( |.e.| + |.n.|) + |.s.|) + 0 ) <= ((( |.e.| + |.n.|) + |.s.|) + |.w.|) by A15, XREAL_1: 7;

          (( |.e.| + |.s.|) + 0 ) <= (( |.e.| + |.s.|) + |.n.|) by A13, XREAL_1: 7;

          then ( |.e.| + |.s.|) <= ((( |.e.| + |.n.|) + |.w.|) + |.s.|) by A25, XXREAL_0: 2;

          then

           A26: ( |.e.| + |.s.|) < r by A3, XXREAL_0: 2;

          

           A27: |.(B `2 ).| <= |.s.| by A8, A24, Th2;

           |.(B `1 ).| <= |.e.| by A6, A24, Th1;

          then ( |.(B `1 ).| + |.(B `2 ).|) <= ( |.e.| + |.s.|) by A27, XREAL_1: 7;

          then ( dist (p,b)) <= ( |.e.| + |.s.|) by A10, A12, XXREAL_0: 2;

          hence ( dist (p,b)) < r by A26, XXREAL_0: 2;

        end;

          case

           A28: (B `1 ) < 0 & (B `2 ) < 0 ;

          then

           A29: |.(B `2 ).| <= |.s.| by A8, Th2;

           |.(B `1 ).| <= |.w.| by A17, A28, Th2;

          then ( |.(B `1 ).| + |.(B `2 ).|) <= ( |.w.| + |.s.|) by A29, XREAL_1: 7;

          then

           A30: ( dist (p,b)) <= ( |.w.| + |.s.|) by A10, A12, XXREAL_0: 2;

          ( 0 + ( |.w.| + |.s.|)) <= (( |.e.| + |.n.|) + ( |.w.| + |.s.|)) by A14, A13, XREAL_1: 7;

          then ( |.w.| + |.s.|) < r by A2, XREAL_1: 8;

          hence ( dist (p,b)) < r by A30, XXREAL_0: 2;

        end;

      end;

      hence thesis by METRIC_1: 11;

    end;

    theorem :: TOPREAL6:53

    

     Th51: for M be Reflexive symmetric triangle non empty MetrStruct, z be Point of M holds r < 0 implies ( Sphere (z,r)) = {}

    proof

      let M be Reflexive symmetric triangle non empty MetrStruct, z be Point of M;

      assume

       A1: r < 0 ;

      thus ( Sphere (z,r)) c= {}

      proof

        let a be object;

        assume

         A2: a in ( Sphere (z,r));

        then

        reconsider b = a as Point of M;

        ( dist (b,z)) = r by A2, METRIC_1: 13;

        hence thesis by A1, METRIC_1: 5;

      end;

      thus thesis;

    end;

    theorem :: TOPREAL6:54

    for M be Reflexive discerning non empty MetrStruct, z be Point of M holds ( Sphere (z, 0 )) = {z}

    proof

      let M be Reflexive discerning non empty MetrStruct, z be Point of M;

      thus ( Sphere (z, 0 )) c= {z}

      proof

        let a be object;

        assume

         A1: a in ( Sphere (z, 0 ));

        then

        reconsider b = a as Point of M;

        ( dist (z,b)) = 0 by A1, METRIC_1: 13;

        then b = z by METRIC_1: 2;

        hence thesis by TARSKI:def 1;

      end;

      let a be object;

      assume a in {z};

      then

       A2: a = z by TARSKI:def 1;

      ( dist (z,z)) = 0 by METRIC_1: 1;

      hence thesis by A2, METRIC_1: 13;

    end;

    theorem :: TOPREAL6:55

    for M be Reflexive symmetric triangle non empty MetrStruct, z be Point of M holds r < 0 implies ( cl_Ball (z,r)) = {}

    proof

      let M be Reflexive symmetric triangle non empty MetrStruct, z be Point of M;

      

       A1: (( Sphere (z,r)) \/ ( Ball (z,r))) = ( cl_Ball (z,r)) by METRIC_1: 16;

      assume

       A2: r < 0 ;

      then ( Ball (z,r)) = {} by TBSP_1: 12;

      hence thesis by A2, A1, Th51;

    end;

    theorem :: TOPREAL6:56

    ( cl_Ball (z, 0 )) = {z}

    proof

      thus ( cl_Ball (z, 0 )) c= {z}

      proof

        let a be object;

        assume

         A1: a in ( cl_Ball (z, 0 ));

        then

        reconsider b = a as Point of M;

        ( dist (b,z)) <= 0 by A1, METRIC_1: 12;

        then ( dist (b,z)) = 0 by METRIC_1: 5;

        then b = z by METRIC_1: 2;

        hence thesis by TARSKI:def 1;

      end;

      let a be object;

      assume a in {z};

      then

       A2: a = z by TARSKI:def 1;

      ( dist (z,z)) = 0 by METRIC_1: 1;

      hence thesis by A2, METRIC_1: 12;

    end;

    

     Lm1: for A be Subset of ( TopSpaceMetr M) st A = ( cl_Ball (z,r)) holds (A ` ) is open

    proof

      let A be Subset of ( TopSpaceMetr M) such that

       A1: A = ( cl_Ball (z,r));

      for x be set holds x in (A ` ) iff ex Q be Subset of ( TopSpaceMetr M) st Q is open & Q c= (A ` ) & x in Q

      proof

        let x be set;

        thus x in (A ` ) implies ex Q be Subset of ( TopSpaceMetr M) st Q is open & Q c= (A ` ) & x in Q

        proof

          assume

           A2: x in (A ` );

          then

          reconsider e = x as Point of M by TOPMETR: 12;

          reconsider Q = ( Ball (e,(( dist (e,z)) - r))) as Subset of ( TopSpaceMetr M) by TOPMETR: 12;

          take Q;

          thus Q is open by TOPMETR: 14;

          thus Q c= (A ` )

          proof

            let q be object;

            assume

             A3: q in Q;

            then

            reconsider f = q as Point of M;

            ( dist (e,z)) <= (( dist (e,f)) + ( dist (f,z))) by METRIC_1: 4;

            then

             A4: (( dist (e,z)) - r) <= ((( dist (e,f)) + ( dist (f,z))) - r) by XREAL_1: 9;

            ( dist (e,f)) < (( dist (e,z)) - r) by A3, METRIC_1: 11;

            then ( dist (e,f)) < ((( dist (e,f)) + ( dist (f,z))) - r) by A4, XXREAL_0: 2;

            then (( dist (e,f)) - ( dist (e,f))) < (((( dist (e,f)) + ( dist (f,z))) - r) - ( dist (e,f))) by XREAL_1: 9;

            then 0 < (((( dist (e,f)) - ( dist (e,f))) + ( dist (f,z))) - r);

            then ( dist (f,z)) > r by XREAL_1: 47;

            then not q in A by A1, METRIC_1: 12;

            hence thesis by A3, SUBSET_1: 29;

          end;

           not x in A by A2, XBOOLE_0:def 5;

          then ( dist (z,e)) > r by A1, METRIC_1: 12;

          then (( dist (e,z)) - r) > (r - r) by XREAL_1: 9;

          hence thesis by TBSP_1: 11;

        end;

        thus thesis;

      end;

      hence thesis by TOPS_1: 25;

    end;

    theorem :: TOPREAL6:57

    

     Th55: for A be Subset of ( TopSpaceMetr M) st A = ( cl_Ball (z,r)) holds A is closed

    proof

      let A be Subset of ( TopSpaceMetr M);

      assume A = ( cl_Ball (z,r));

      then (A ` ) is open by Lm1;

      hence thesis by TOPS_1: 3;

    end;

    theorem :: TOPREAL6:58

    A = ( cl_Ball (w,r)) implies A is closed

    proof

      

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

      then

      reconsider E = A as Subset of ( TopSpaceMetr ( Euclid n));

      assume A = ( cl_Ball (w,r));

      then E is closed by Th55;

      hence A is closed by A1, PRE_TOPC: 31;

    end;

    theorem :: TOPREAL6:59

    

     Th57: for r be Real holds for M be Reflexive symmetric triangle non empty MetrStruct holds for x be Element of M holds ( cl_Ball (x,r)) is bounded

    proof

      let r be Real;

      let M be Reflexive symmetric triangle non empty MetrStruct;

      let x be Element of M;

      ( cl_Ball (x,r)) c= ( Ball (x,(r + 1)))

      proof

        let y be object such that

         A1: y in ( cl_Ball (x,r));

        reconsider Y = y as Point of M by A1;

        

         A2: (r + 0 ) < (r + 1) by XREAL_1: 8;

        ( dist (x,Y)) <= r by A1, METRIC_1: 12;

        then ( dist (x,Y)) < (r + 1) by A2, XXREAL_0: 2;

        hence thesis by METRIC_1: 11;

      end;

      hence thesis by TBSP_1: 14;

    end;

    theorem :: TOPREAL6:60

    

     Th58: for A be Subset of ( TopSpaceMetr M) st A = ( Sphere (z,r)) holds A is closed

    proof

      let A be Subset of ( TopSpaceMetr M) such that

       A1: A = ( Sphere (z,r));

      reconsider B = ( cl_Ball (z,r)), C = ( Ball (z,r)) as Subset of ( TopSpaceMetr M) by TOPMETR: 12;

      

       A2: (( cl_Ball (z,r)) ` ) = (B ` ) by TOPMETR: 12;

      

       A3: (A ` ) = ((B ` ) \/ C)

      proof

        hereby

          let a be object;

          assume

           A4: a in (A ` );

          then

          reconsider e = a as Point of M by TOPMETR: 12;

           not a in A by A4, XBOOLE_0:def 5;

          then ( dist (e,z)) <> r by A1, METRIC_1: 13;

          then ( dist (e,z)) < r or ( dist (e,z)) > r by XXREAL_0: 1;

          then e in ( Ball (z,r)) or not e in ( cl_Ball (z,r)) by METRIC_1: 11, METRIC_1: 12;

          then e in ( Ball (z,r)) or e in (( cl_Ball (z,r)) ` ) by SUBSET_1: 29;

          hence a in ((B ` ) \/ C) by A2, XBOOLE_0:def 3;

        end;

        let a be object;

        assume

         A5: a in ((B ` ) \/ C);

        then

        reconsider e = a as Point of M by TOPMETR: 12;

        a in (B ` ) or a in C by A5, XBOOLE_0:def 3;

        then not e in ( cl_Ball (z,r)) or e in C by XBOOLE_0:def 5;

        then ( dist (e,z)) > r or ( dist (e,z)) < r by METRIC_1: 11, METRIC_1: 12;

        then not a in A by A1, METRIC_1: 13;

        hence thesis by A5, SUBSET_1: 29;

      end;

      

       A6: C is open by TOPMETR: 14;

      (B ` ) is open by Lm1;

      hence thesis by A3, A6, TOPS_1: 3;

    end;

    theorem :: TOPREAL6:61

    A = ( Sphere (w,r)) implies A is closed

    proof

      

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

      then

      reconsider E = A as Subset of ( TopSpaceMetr ( Euclid n));

      assume A = ( Sphere (w,r));

      then E is closed by Th58;

      hence A is closed by A1, PRE_TOPC: 31;

    end;

    theorem :: TOPREAL6:62

    ( Sphere (z,r)) is bounded

    proof

      ( Sphere (z,r)) c= ( cl_Ball (z,r)) by METRIC_1: 15;

      hence thesis by Th57, TBSP_1: 14;

    end;

    theorem :: TOPREAL6:63

    A is bounded implies ( Cl A) is bounded;

    theorem :: TOPREAL6:64

    for M be non empty MetrStruct holds M is bounded iff for X be Subset of M holds X is bounded

    proof

      let M be non empty MetrStruct;

      hereby

        assume

         A1: M is bounded;

        let X be Subset of M;

        ( [#] M) is bounded by A1;

        hence X is bounded by TBSP_1: 14;

      end;

      assume for X be Subset of M holds X is bounded;

      then ( [#] M) is bounded;

      hence thesis by TBSP_1: 18;

    end;

    theorem :: TOPREAL6:65

    

     Th63: for M be Reflexive symmetric triangle non empty MetrStruct, X,Y be Subset of M st the carrier of M = (X \/ Y) & M is non bounded & X is bounded holds Y is non bounded

    proof

      let M be Reflexive symmetric triangle non empty MetrStruct, X,Y be Subset of M such that

       A1: the carrier of M = (X \/ Y) and

       A2: M is non bounded;

      assume that

       A3: X is bounded and

       A4: Y is bounded;

      ( [#] M) is bounded by A1, A3, A4, TBSP_1: 13;

      hence thesis by A2, TBSP_1: 18;

    end;

    theorem :: TOPREAL6:66

    for X,Y be Subset of ( TOP-REAL n) st n >= 1 & the carrier of ( TOP-REAL n) = (X \/ Y) & X is bounded holds Y is non bounded

    proof

      set M = ( TOP-REAL n);

      let X,Y be Subset of M such that

       A1: n >= 1 and

       A2: the carrier of M = (X \/ Y);

      reconsider E = ( [#] M) as Subset of ( Euclid n) by TOPREAL3: 8;

      ( [#] ( TOP-REAL n)) is non bounded by A1, JORDAN2C: 35;

      then

       A3: E is non bounded by JORDAN2C: 11;

      reconsider D = Y as Subset of ( Euclid n) by TOPREAL3: 8;

      assume X is bounded;

      then

      reconsider C = X as bounded Subset of ( Euclid n) by JORDAN2C: 11;

      

       A4: the carrier of ( Euclid n) = (C \/ D) by A2, TOPREAL3: 8;

      E = ( [#] ( Euclid n)) by TOPREAL3: 8;

      then ( Euclid n) is non bounded by A3;

      then D is non bounded by A4, Th63;

      hence thesis by JORDAN2C: 11;

    end;

    theorem :: TOPREAL6:67

    

     Th65: A is bounded & B is bounded implies (A \/ B) is bounded

    proof

      assume A is bounded;

      then

       A1: A is bounded Subset of ( Euclid n) by JORDAN2C: 11;

      then

      reconsider A as Subset of ( Euclid n);

      assume B is bounded;

      then

       A2: B is bounded Subset of ( Euclid n) by JORDAN2C: 11;

      then

      reconsider B as Subset of ( Euclid n);

      reconsider E = (A \/ B) as Subset of ( Euclid n);

      E is bounded Subset of ( Euclid n) by A1, A2, TBSP_1: 13;

      hence thesis by JORDAN2C: 11;

    end;

    begin

    registration

      let X be non empty Subset of REAL ;

      cluster ( Cl X) -> non empty;

      coherence by MEASURE6: 58, XBOOLE_1: 3;

    end

    registration

      let D be bounded_below Subset of REAL ;

      cluster ( Cl D) -> bounded_below;

      coherence

      proof

        consider p be Real such that

         A1: p is LowerBound of D by XXREAL_2:def 9;

        

         A2: for r be Real st r in D holds p <= r by A1, XXREAL_2:def 2;

        take p;

        let r be ExtReal;

        assume r in ( Cl D);

        then

        consider s be Real_Sequence such that

         A3: ( rng s) c= D and

         A4: s is convergent and

         A5: ( lim s) = r by MEASURE6: 64;

        for n holds (s . n) >= p

        proof

          let n;

          

           A6: n in NAT by ORDINAL1:def 12;

          ( dom s) = NAT by FUNCT_2:def 1;

          then (s . n) in ( rng s) by A6, FUNCT_1:def 3;

          hence thesis by A2, A3;

        end;

        hence thesis by A4, A5, PREPOWER: 1;

      end;

    end

    registration

      let D be bounded_above Subset of REAL ;

      cluster ( Cl D) -> bounded_above;

      coherence

      proof

        consider p be Real such that

         A1: p is UpperBound of D by XXREAL_2:def 10;

        

         A2: for r be Real st r in D holds r <= p by A1, XXREAL_2:def 1;

        take p;

        let r be ExtReal;

        assume r in ( Cl D);

        then

        consider s be Real_Sequence such that

         A3: ( rng s) c= D and

         A4: s is convergent and

         A5: ( lim s) = r by MEASURE6: 64;

        for n holds (s . n) <= p

        proof

          let n;

          

           A6: n in NAT by ORDINAL1:def 12;

          ( dom s) = NAT by FUNCT_2:def 1;

          then (s . n) in ( rng s) by A6, FUNCT_1:def 3;

          hence thesis by A2, A3;

        end;

        hence thesis by A4, A5, PREPOWER: 2;

      end;

    end

    theorem :: TOPREAL6:68

    

     Th66: for D be non empty bounded_below Subset of REAL holds ( lower_bound D) = ( lower_bound ( Cl D))

    proof

      let D be non empty bounded_below Subset of REAL ;

      

       A1: for q be Real st for p be Real st p in D holds p >= q holds ( lower_bound ( Cl D)) >= q

      proof

        let q be Real such that

         A2: for p be Real st p in D holds p >= q;

        for p be Real st p in ( Cl D) holds p >= q

        proof

          let p be Real;

          assume p in ( Cl D);

          then

          consider s be Real_Sequence such that

           A3: ( rng s) c= D and

           A4: s is convergent and

           A5: ( lim s) = p by MEASURE6: 64;

          for n holds (s . n) >= q

          proof

            let n;

            

             A6: n in NAT by ORDINAL1:def 12;

            ( dom s) = NAT by FUNCT_2:def 1;

            then (s . n) in ( rng s) by A6, FUNCT_1:def 3;

            hence thesis by A2, A3;

          end;

          hence thesis by A4, A5, PREPOWER: 1;

        end;

        hence thesis by SEQ_4: 43;

      end;

      

       A7: ( lower_bound ( Cl D)) <= ( lower_bound D) by MEASURE6: 58, SEQ_4: 47;

      for p be Real st p in D holds p >= ( lower_bound ( Cl D))

      proof

        let p be Real;

        assume p in D;

        then ( lower_bound D) <= p by SEQ_4:def 2;

        hence thesis by A7, XXREAL_0: 2;

      end;

      hence thesis by A1, SEQ_4: 44;

    end;

    theorem :: TOPREAL6:69

    

     Th67: for D be non empty bounded_above Subset of REAL holds ( upper_bound D) = ( upper_bound ( Cl D))

    proof

      let D be non empty bounded_above Subset of REAL ;

      

       A1: for q be Real st for p be Real st p in D holds p <= q holds ( upper_bound ( Cl D)) <= q

      proof

        let q be Real such that

         A2: for p be Real st p in D holds p <= q;

        for p be Real st p in ( Cl D) holds p <= q

        proof

          let p be Real;

          assume p in ( Cl D);

          then

          consider s be Real_Sequence such that

           A3: ( rng s) c= D and

           A4: s is convergent and

           A5: ( lim s) = p by MEASURE6: 64;

          for n holds (s . n) <= q

          proof

            let n;

            

             A6: n in NAT by ORDINAL1:def 12;

            ( dom s) = NAT by FUNCT_2:def 1;

            then (s . n) in ( rng s) by A6, FUNCT_1:def 3;

            hence thesis by A2, A3;

          end;

          hence thesis by A4, A5, PREPOWER: 2;

        end;

        hence thesis by SEQ_4: 45;

      end;

      

       A7: ( upper_bound ( Cl D)) >= ( upper_bound D) by MEASURE6: 58, SEQ_4: 48;

      for p be Real st p in D holds p <= ( upper_bound ( Cl D))

      proof

        let p be Real;

        assume p in D;

        then ( upper_bound D) >= p by SEQ_4:def 1;

        hence thesis by A7, XXREAL_0: 2;

      end;

      hence thesis by A1, SEQ_4: 46;

    end;

    registration

      cluster R^1 -> T_2;

      coherence by PCOMPS_1: 34, TOPMETR:def 6;

    end

    ::$Canceled

    theorem :: TOPREAL6:75

    

     Th68: for A,B be Subset of REAL , f be Function of [: R^1 , R^1 :], ( TOP-REAL 2) st for x,y be Real holds (f . [x, y]) = <*x, y*> holds (f .: [:A, B:]) = ( product ((1,2) --> (A,B)))

    proof

      let A,B be Subset of REAL , f be Function of [: R^1 , R^1 :], ( TOP-REAL 2) such that

       A1: for x,y be Real holds (f . [x, y]) = <*x, y*>;

      set h = ((1,2) --> (A,B));

      

       A2: ( dom h) = {1, 2} by FUNCT_4: 62;

      thus (f .: [:A, B:]) c= ( product h)

      proof

        let x be object;

        assume x in (f .: [:A, B:]);

        then

        consider a be object such that

         A3: a in the carrier of [: R^1 , R^1 :] and

         A4: a in [:A, B:] and

         A5: (f . a) = x by FUNCT_2: 64;

        reconsider a as Point of [: R^1 , R^1 :] by A3;

        consider m,n be object such that

         A6: m in A and

         A7: n in B and

         A8: a = [m, n] by A4, ZFMISC_1:def 2;

        (f . a) = x by A5;

        then

        reconsider g = x as Function of ( Seg 2), REAL by EUCLID: 23;

        reconsider m, n as Real by A6, A7;

        

         A9: for y be object st y in ( dom h) holds (g . y) in (h . y)

        proof

          let y be object;

          

           A10: ( |[m, n]| `1 ) = m by EUCLID: 52;

          assume y in ( dom h);

          then

           A11: y = 1 or y = 2 by TARSKI:def 2;

          

           A12: ( |[m, n]| `2 ) = n by EUCLID: 52;

          (f . [m, n]) = |[m, n]| by A1;

          hence thesis by A5, A6, A7, A8, A11, A10, A12, FUNCT_4: 63;

        end;

        ( dom g) = ( dom h) by A2, FINSEQ_1: 2, FUNCT_2:def 1;

        hence thesis by A9, CARD_3: 9;

      end;

      

       A13: (h . 2) = B by FUNCT_4: 63;

      let a be object;

      assume a in ( product h);

      then

      consider g be Function such that

       A14: a = g and

       A15: ( dom g) = ( dom h) and

       A16: for x be object st x in ( dom h) holds (g . x) in (h . x) by CARD_3:def 5;

      2 in ( dom h) by A2, TARSKI:def 2;

      then

       A17: (g . 2) in B by A13, A16;

      

       A18: (h . 1) = A by FUNCT_4: 63;

      1 in ( dom h) by A2, TARSKI:def 2;

      then

       A19: (g . 1) in A by A18, A16;

      then

       A20: (f . [(g . 1), (g . 2)]) = <*(g . 1), (g . 2)*> by A1, A17;

       A21:

      now

        let k be object;

        assume k in ( dom g);

        then k = 1 or k = 2 by A15, TARSKI:def 2;

        hence (g . k) = ( <*(g . 1), (g . 2)*> . k) by FINSEQ_1: 44;

      end;

      

       A22: ( dom <*(g . 1), (g . 2)*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      

       A23: [(g . 1), (g . 2)] in [:A, B:] by A19, A17, ZFMISC_1: 87;

      the carrier of [: R^1 , R^1 :] = [:the carrier of R^1 , the carrier of R^1 :] by BORSUK_1:def 2;

      then [(g . 1), (g . 2)] in the carrier of [: R^1 , R^1 :] by A19, A17, TOPMETR: 17, ZFMISC_1: 87;

      hence thesis by A2, A14, A15, A23, A22, A21, A20, FUNCT_1: 2, FUNCT_2: 35;

    end;

    theorem :: TOPREAL6:76

    

     Th69: for f be Function of [: R^1 , R^1 :], ( TOP-REAL 2) st for x,y be Real holds (f . [x, y]) = <*x, y*> holds f is being_homeomorphism

    proof

      reconsider f1 = proj1 , f2 = proj2 as Function of ( TOP-REAL 2), R^1 by TOPMETR: 17;

      let f be Function of [: R^1 , R^1 :], ( TOP-REAL 2) such that

       A1: for x,y be Real holds (f . [x, y]) = <*x, y*>;

      thus ( dom f) = ( [#] [: R^1 , R^1 :]) by FUNCT_2:def 1;

      

       A2: the carrier of [: R^1 , R^1 :] = [:the carrier of R^1 , the carrier of R^1 :] by BORSUK_1:def 2;

      then

       A3: ( dom f) = [:the carrier of R^1 , the carrier of R^1 :] by FUNCT_2:def 1;

      thus

       A4: ( rng f) = ( [#] ( TOP-REAL 2))

      proof

        thus ( rng f) c= ( [#] ( TOP-REAL 2));

        let y be object;

        assume y in ( [#] ( TOP-REAL 2));

        then

        consider a,b be Element of REAL such that

         A5: y = <*a, b*> by EUCLID: 51;

        

         A6: (f . [a, b]) = <*a, b*> by A1;

        reconsider a, b as Element of REAL ;

         [a, b] in ( dom f) by A3, TOPMETR: 17, ZFMISC_1: 87;

        hence thesis by A5, A6, FUNCT_1:def 3;

      end;

      thus

       A7: f is one-to-one

      proof

        let x,y be object;

        assume x in ( dom f);

        then

        consider x1,x2 be object such that

         A8: x1 in REAL and

         A9: x2 in REAL and

         A10: x = [x1, x2] by A2, TOPMETR: 17, ZFMISC_1:def 2;

        assume y in ( dom f);

        then

        consider y1,y2 be object such that

         A11: y1 in REAL and

         A12: y2 in REAL and

         A13: y = [y1, y2] by A2, TOPMETR: 17, ZFMISC_1:def 2;

        reconsider x1, x2, y1, y2 as Real by A8, A9, A11, A12;

        assume

         A14: (f . x) = (f . y);

        

         A15: (f . [y1, y2]) = <*y1, y2*> by A1;

        

         A16: (f . [x1, x2]) = <*x1, x2*> by A1;

        then x1 = y1 by A10, A13, A15, A14, FINSEQ_1: 77;

        hence thesis by A10, A13, A16, A15, A14, FINSEQ_1: 77;

      end;

       A17:

      now

        

         A18: ( dom f2) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

        let x be object;

        

         A19: ( dom f1) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

        assume

         A20: x in ( dom (f " ));

        then

        consider a,b be Element of REAL such that

         A21: x = <*a, b*> by EUCLID: 51;

        reconsider a, b as Element of REAL ;

        reconsider p = x as Point of ( TOP-REAL 2) by A20;

        

         A22: [a, b] in ( dom f) by A3, TOPMETR: 17, ZFMISC_1: 87;

        

         A23: (f . [a, b]) = <*a, b*> by A1;

        f is onto by A4, FUNCT_2:def 3;

        

        hence ((f " ) . x) = ((f qua Function " ) . x) by A7, TOPS_2:def 4

        .= [a, b] by A7, A21, A22, A23, FUNCT_1: 32

        .= [(p `1 ), b] by A21, EUCLID: 52

        .= [(p `1 ), (p `2 )] by A21, EUCLID: 52

        .= [(f1 . x), (p `2 )] by PSCOMP_1:def 5

        .= [(f1 . x), (f2 . x)] by PSCOMP_1:def 6

        .= ( <:f1, f2:> . x) by A20, A19, A18, FUNCT_3: 49;

      end;

      thus f is continuous

      proof

        let w be Point of [: R^1 , R^1 :], G be a_neighborhood of (f . w);

        reconsider fw = (f . w) as Point of ( Euclid 2) by TOPREAL3: 8;

        consider x,y be object such that

         A24: x in the carrier of R^1 and

         A25: y in the carrier of R^1 and

         A26: w = [x, y] by A2, ZFMISC_1:def 2;

        reconsider x, y as Real by A24, A25;

        fw in ( Int G) by CONNSP_2:def 1;

        then

        consider r be Real such that

         A27: r > 0 and

         A28: ( Ball (fw,r)) c= G by GOBOARD6: 5;

        reconsider r as Real;

        set A = ].(((f . w) `1 ) - (r / ( sqrt 2))), (((f . w) `1 ) + (r / ( sqrt 2))).[, B = ].(((f . w) `2 ) - (r / ( sqrt 2))), (((f . w) `2 ) + (r / ( sqrt 2))).[;

        reconsider A, B as Subset of R^1 by TOPMETR: 17;

        

         A29: (f . [x, y]) = <*x, y*> by A1;

        then y = ((f . w) `2 ) by A26, EUCLID: 52;

        then

         A30: y in B by A27, Th14, SQUARE_1: 19, XREAL_1: 139;

        x = ((f . w) `1 ) by A26, A29, EUCLID: 52;

        then x in A by A27, Th14, SQUARE_1: 19, XREAL_1: 139;

        then

         A31: w in [:A, B:] by A26, A30, ZFMISC_1: 87;

        take [:A, B:];

        

         A32: B is open by JORDAN6: 35;

        A is open by JORDAN6: 35;

        then [:A, B:] in ( Base-Appr [:A, B:]) by A32;

        then w in ( union ( Base-Appr [:A, B:])) by A31, TARSKI:def 4;

        then w in ( Int [:A, B:]) by BORSUK_1: 14;

        hence [:A, B:] is a_neighborhood of w by CONNSP_2:def 1;

        ( product ((1,2) --> (A,B))) c= ( Ball (fw,r)) by Th39;

        then (f .: [:A, B:]) c= ( Ball (fw,r)) by A1, Th68;

        hence thesis by A28;

      end;

      

       A33: f1 is continuous by JORDAN5A: 27;

      

       A34: f2 is continuous by JORDAN5A: 27;

      ( dom <:f1, f2:>) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

      then (f " ) = <:f1, f2:> by A4, A7, A17, TOPS_2: 49;

      hence thesis by A33, A34, YELLOW12: 41;

    end;

    theorem :: TOPREAL6:77

    ( [: R^1 , R^1 :],( TOP-REAL 2)) are_homeomorphic

    proof

      defpred P[ Real, Real, set] means ex c be Element of ( REAL 2) st c = $3 & $3 = <*$1, $2*>;

      

       A1: the carrier of ( TOP-REAL 2) = ( REAL 2) by EUCLID: 22;

      

       A2: for x,y be Element of REAL holds ex u be Element of ( REAL 2) st P[x, y, u]

      proof

        let x,y be Element of REAL ;

        take <*x, y*>;

        thus <*x, y*> is Element of ( REAL 2) by FINSEQ_2: 137;

         <*x, y*> in (2 -tuples_on REAL ) by FINSEQ_2: 137;

        hence thesis;

      end;

      consider f be Function of [: REAL , REAL :], ( REAL 2) such that

       A3: for x,y be Element of REAL holds P[x, y, (f . (x,y))] from BINOP_1:sch 3( A2);

      the carrier of [: R^1 , R^1 :] = [:the carrier of R^1 , the carrier of R^1 :] by BORSUK_1:def 2;

      then

      reconsider f as Function of [: R^1 , R^1 :], ( TOP-REAL 2) by A1, TOPMETR: 17;

      take f;

      for x,y be Real holds (f . [x, y]) = <*x, y*>

      proof

        let x,y be Real;

        x in REAL & y in REAL by XREAL_0:def 1;

        then P[x, y, (f . (x,y))] by A3;

        hence thesis;

      end;

      hence thesis by Th69;

    end;

    begin

    theorem :: TOPREAL6:78

    

     Th71: for A,B be compact Subset of REAL holds ( product ((1,2) --> (A,B))) is compact Subset of ( TOP-REAL 2)

    proof

      defpred P[ Real, Real, set] means ex c be Element of ( REAL 2) st c = $3 & $3 = <*$1, $2*>;

      let A,B be compact Subset of REAL ;

      reconsider X = ( product ((1,2) --> (A,B))) as Subset of ( TOP-REAL 2) by Th20;

      reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR: 17;

      

       A1: the carrier of ( TOP-REAL 2) = ( REAL 2) by EUCLID: 22;

      

       A2: for x,y be Element of REAL holds ex u be Element of ( REAL 2) st P[x, y, u]

      proof

        let x,y be Element of REAL ;

        take <*x, y*>;

        thus <*x, y*> is Element of ( REAL 2) by FINSEQ_2: 137;

         <*x, y*> in (2 -tuples_on REAL ) by FINSEQ_2: 137;

        hence thesis;

      end;

      consider h be Function of [: REAL , REAL :], ( REAL 2) such that

       A3: for x,y be Element of REAL holds P[x, y, (h . (x,y))] from BINOP_1:sch 3( A2);

      the carrier of [: R^1 , R^1 :] = [:the carrier of R^1 , the carrier of R^1 :] by BORSUK_1:def 2;

      then

      reconsider h as Function of [: R^1 , R^1 :], ( TOP-REAL 2) by A1, TOPMETR: 17;

      

       A4: for x,y be Real holds (h . [x, y]) = <*x, y*>

      proof

        let x,y be Real;

        x in REAL & y in REAL by XREAL_0:def 1;

        then P[x, y, (h . (x,y))] by A3;

        hence thesis;

      end;

      then

       A5: h is being_homeomorphism by Th69;

      

       A6: B1 is compact by JORDAN5A: 25;

      A1 is compact by JORDAN5A: 25;

      then

       A7: [:A1, B1:] is compact by A6, BORSUK_3: 23;

      (h .: [:A1, B1:]) = X by A4, Th68;

      hence thesis by A7, A5, WEIERSTR: 8;

    end;

    theorem :: TOPREAL6:79

    

     Th72: P is bounded closed implies P is compact

    proof

      assume

       A1: P is bounded closed;

      then

      reconsider C = P as bounded Subset of ( Euclid 2) by JORDAN2C: 11;

      consider r be Real, e such that 0 < r and

       A2: C c= ( Ball (e,r)) by METRIC_6:def 3;

      reconsider p = e as Point of ( TOP-REAL 2) by TOPREAL3: 8;

      

       A3: ].((p `2 ) - r), ((p `2 ) + r).[ c= [.((p `2 ) - r), ((p `2 ) + r).] by XXREAL_1: 25;

      

       A4: ( Ball (e,r)) c= ( product ((1,2) --> ( ].((p `1 ) - r), ((p `1 ) + r).[, ].((p `2 ) - r), ((p `2 ) + r).[))) by Th40;

       ].((p `1 ) - r), ((p `1 ) + r).[ c= [.((p `1 ) - r), ((p `1 ) + r).] by XXREAL_1: 25;

      then ( product ((1,2) --> ( ].((p `1 ) - r), ((p `1 ) + r).[, ].((p `2 ) - r), ((p `2 ) + r).[))) c= ( product ((1,2) --> ( [.((p `1 ) - r), ((p `1 ) + r).], [.((p `2 ) - r), ((p `2 ) + r).]))) by A3, Th19;

      then

       A5: ( Ball (e,r)) c= ( product ((1,2) --> ( [.((p `1 ) - r), ((p `1 ) + r).], [.((p `2 ) - r), ((p `2 ) + r).]))) by A4;

      ( product ((1,2) --> ( [.((p `1 ) - r), ((p `1 ) + r).], [.((p `2 ) - r), ((p `2 ) + r).]))) is compact Subset of ( TOP-REAL 2) by Th71;

      hence thesis by A1, A2, A5, COMPTS_1: 9, XBOOLE_1: 1;

    end;

    theorem :: TOPREAL6:80

    

     Th73: P is bounded implies for g be continuous RealMap of ( TOP-REAL 2) holds ( Cl (g .: P)) c= (g .: ( Cl P))

    proof

      assume P is bounded;

      then

       A1: ( Cl P) is compact by Th72;

      let g be continuous RealMap of ( TOP-REAL 2);

      reconsider f = g as Function of ( TOP-REAL 2), R^1 by TOPMETR: 17;

      f is continuous by JORDAN5A: 27;

      then (f .: ( Cl P)) is closed by A1, COMPTS_1: 7, WEIERSTR: 9;

      then

       A2: (g .: ( Cl P)) is closed by JORDAN5A: 23;

      (g .: P) c= (g .: ( Cl P)) by PRE_TOPC: 18, RELAT_1: 123;

      hence thesis by A2, MEASURE6: 57;

    end;

    theorem :: TOPREAL6:81

    

     Th74: ( proj1 .: ( Cl P)) c= ( Cl ( proj1 .: P))

    proof

      let y be object;

      assume y in ( proj1 .: ( Cl P));

      then

      consider x be object such that

       A1: x in the carrier of ( TOP-REAL 2) and

       A2: x in ( Cl P) and

       A3: y = ( proj1 . x) by FUNCT_2: 64;

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

      set r = ( proj1 . x);

      for O be open Subset of REAL st y in O holds (O /\ ( proj1 .: P)) is non empty

      proof

        reconsider e = x as Point of ( Euclid 2) by TOPREAL3: 8;

        let O be open Subset of REAL ;

        assume y in O;

        then

        consider g be Real such that

         A4: 0 < g and

         A5: ].(r - g), (r + g).[ c= O by A3, RCOMP_1: 19;

        reconsider g as Real;

        reconsider B = ( Ball (e,(g / 2))) as Subset of ( TOP-REAL 2) by TOPREAL3: 8;

        

         A6: B is open by GOBOARD6: 3;

        e in B by A4, TBSP_1: 11, XREAL_1: 139;

        then P meets B by A2, A6, TOPS_1: 12;

        then (P /\ B) <> {} ;

        then

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

         A7: d in (P /\ B) by SUBSET_1: 4;

        

         A8: d in B by A7, XBOOLE_0:def 4;

        then ((x `1 ) - (g / 2)) < (d `1 ) by Th37;

        then

         A9: (r - (g / 2)) < (d `1 ) by PSCOMP_1:def 5;

        (d `1 ) < ((x `1 ) + (g / 2)) by A8, Th37;

        then

         A10: (d `1 ) < (r + (g / 2)) by PSCOMP_1:def 5;

        d in P by A7, XBOOLE_0:def 4;

        then ( proj1 . d) in ( proj1 .: P) by FUNCT_2: 35;

        then

         A11: (d `1 ) in ( proj1 .: P) by PSCOMP_1:def 5;

        

         A12: (g / 2) < (g / 1) by A4, XREAL_1: 76;

        then (r - g) < (r - (g / 2)) by XREAL_1: 15;

        then

         A13: (r - g) < (d `1 ) by A9, XXREAL_0: 2;

        (r + (g / 2)) < (r + g) by A12, XREAL_1: 6;

        then

         A14: (d `1 ) < (r + g) by A10, XXREAL_0: 2;

         ].(r - g), (r + g).[ = { t where t be Real : (r - g) < t & t < (r + g) } by RCOMP_1:def 2;

        then (d `1 ) in ].(r - g), (r + g).[ by A13, A14;

        hence thesis by A5, A11, XBOOLE_0:def 4;

      end;

      hence thesis by A3, MEASURE6: 63;

    end;

    theorem :: TOPREAL6:82

    

     Th75: ( proj2 .: ( Cl P)) c= ( Cl ( proj2 .: P))

    proof

      let y be object;

      assume y in ( proj2 .: ( Cl P));

      then

      consider x be object such that

       A1: x in the carrier of ( TOP-REAL 2) and

       A2: x in ( Cl P) and

       A3: y = ( proj2 . x) by FUNCT_2: 64;

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

      set r = ( proj2 . x);

      for O be open Subset of REAL st y in O holds (O /\ ( proj2 .: P)) is non empty

      proof

        reconsider e = x as Point of ( Euclid 2) by TOPREAL3: 8;

        let O be open Subset of REAL ;

        assume y in O;

        then

        consider g be Real such that

         A4: 0 < g and

         A5: ].(r - g), (r + g).[ c= O by A3, RCOMP_1: 19;

        reconsider g as Real;

        reconsider B = ( Ball (e,(g / 2))) as Subset of ( TOP-REAL 2) by TOPREAL3: 8;

        

         A6: B is open by GOBOARD6: 3;

        e in B by A4, TBSP_1: 11, XREAL_1: 139;

        then P meets B by A2, A6, TOPS_1: 12;

        then (P /\ B) <> {} ;

        then

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

         A7: d in (P /\ B) by SUBSET_1: 4;

        

         A8: d in B by A7, XBOOLE_0:def 4;

        then ((x `2 ) - (g / 2)) < (d `2 ) by Th38;

        then

         A9: (r - (g / 2)) < (d `2 ) by PSCOMP_1:def 6;

        (d `2 ) < ((x `2 ) + (g / 2)) by A8, Th38;

        then

         A10: (d `2 ) < (r + (g / 2)) by PSCOMP_1:def 6;

        d in P by A7, XBOOLE_0:def 4;

        then ( proj2 . d) in ( proj2 .: P) by FUNCT_2: 35;

        then

         A11: (d `2 ) in ( proj2 .: P) by PSCOMP_1:def 6;

        

         A12: (g / 2) < (g / 1) by A4, XREAL_1: 76;

        then (r - g) < (r - (g / 2)) by XREAL_1: 15;

        then

         A13: (r - g) < (d `2 ) by A9, XXREAL_0: 2;

        (r + (g / 2)) < (r + g) by A12, XREAL_1: 6;

        then

         A14: (d `2 ) < (r + g) by A10, XXREAL_0: 2;

         ].(r - g), (r + g).[ = { t where t be Real : (r - g) < t & t < (r + g) } by RCOMP_1:def 2;

        then (d `2 ) in ].(r - g), (r + g).[ by A13, A14;

        hence thesis by A5, A11, XBOOLE_0:def 4;

      end;

      hence thesis by A3, MEASURE6: 63;

    end;

    theorem :: TOPREAL6:83

    

     Th76: P is bounded implies ( Cl ( proj1 .: P)) = ( proj1 .: ( Cl P)) by Th73, Th74;

    theorem :: TOPREAL6:84

    

     Th77: P is bounded implies ( Cl ( proj2 .: P)) = ( proj2 .: ( Cl P)) by Th73, Th75;

    theorem :: TOPREAL6:85

    D is bounded implies ( W-bound D) = ( W-bound ( Cl D))

    proof

      

       A1: D c= ( Cl D) by PRE_TOPC: 18;

      assume

       A2: D is bounded;

      then ( Cl D) is compact by Th72;

      then ( proj1 .: ( Cl D)) is bounded_below;

      then ( proj1 .: D) is bounded_below by A1, RELAT_1: 123, XXREAL_2: 44;

      

      then

       A3: ( lower_bound ( proj1 .: D)) = ( lower_bound ( Cl ( proj1 .: D))) by Th66

      .= ( lower_bound ( proj1 .: ( Cl D))) by A2, Th76;

      ( W-bound D) = ( lower_bound ( proj1 .: D)) by SPRECT_1: 43;

      hence thesis by A3, SPRECT_1: 43;

    end;

    theorem :: TOPREAL6:86

    D is bounded implies ( E-bound D) = ( E-bound ( Cl D))

    proof

      

       A1: D c= ( Cl D) by PRE_TOPC: 18;

      assume

       A2: D is bounded;

      then ( Cl D) is compact by Th72;

      then ( proj1 .: ( Cl D)) is bounded_above;

      then ( proj1 .: D) is bounded_above by A1, RELAT_1: 123, XXREAL_2: 43;

      

      then

       A3: ( upper_bound ( proj1 .: D)) = ( upper_bound ( Cl ( proj1 .: D))) by Th67

      .= ( upper_bound ( proj1 .: ( Cl D))) by A2, Th76;

      ( E-bound D) = ( upper_bound ( proj1 .: D)) by SPRECT_1: 46;

      hence thesis by A3, SPRECT_1: 46;

    end;

    theorem :: TOPREAL6:87

    D is bounded implies ( N-bound D) = ( N-bound ( Cl D))

    proof

      

       A1: D c= ( Cl D) by PRE_TOPC: 18;

      assume

       A2: D is bounded;

      then ( Cl D) is compact by Th72;

      then ( proj2 .: ( Cl D)) is bounded_above;

      then ( proj2 .: D) is bounded_above by A1, RELAT_1: 123, XXREAL_2: 43;

      

      then

       A3: ( upper_bound ( proj2 .: D)) = ( upper_bound ( Cl ( proj2 .: D))) by Th67

      .= ( upper_bound ( proj2 .: ( Cl D))) by A2, Th77;

      ( N-bound D) = ( upper_bound ( proj2 .: D)) by SPRECT_1: 45;

      hence thesis by A3, SPRECT_1: 45;

    end;

    theorem :: TOPREAL6:88

    D is bounded implies ( S-bound D) = ( S-bound ( Cl D))

    proof

      

       A1: D c= ( Cl D) by PRE_TOPC: 18;

      assume

       A2: D is bounded;

      then ( Cl D) is compact by Th72;

      then ( proj2 .: ( Cl D)) is bounded_below;

      then ( proj2 .: D) is bounded_below by A1, RELAT_1: 123, XXREAL_2: 44;

      

      then

       A3: ( lower_bound ( proj2 .: D)) = ( lower_bound ( Cl ( proj2 .: D))) by Th66

      .= ( lower_bound ( proj2 .: ( Cl D))) by A2, Th77;

      ( S-bound D) = ( lower_bound ( proj2 .: D)) by SPRECT_1: 44;

      hence thesis by A3, SPRECT_1: 44;

    end;

    theorem :: TOPREAL6:89

    

     Th82: for A,B be Subset of ( TOP-REAL n) holds A is bounded or B is bounded implies (A /\ B) is bounded

    proof

      let A,B be Subset of ( TOP-REAL n);

      assume

       A1: A is bounded or B is bounded;

      per cases by A1;

        suppose A is bounded;

        hence thesis by RLTOPSP1: 42, XBOOLE_1: 17;

      end;

        suppose B is bounded;

        hence thesis by RLTOPSP1: 42, XBOOLE_1: 17;

      end;

    end;

    theorem :: TOPREAL6:90

    for A,B be Subset of ( TOP-REAL n) holds not A is bounded & B is bounded implies not (A \ B) is bounded

    proof

      let A,B be Subset of ( TOP-REAL n);

      assume that

       A1: not A is bounded and

       A2: B is bounded;

      

       A3: ((A \ B) \/ (A /\ B)) = (A \ (B \ B)) by XBOOLE_1: 52

      .= (A \ {} ) by XBOOLE_1: 37

      .= A;

      (A /\ B) is bounded by A2, Th82;

      hence thesis by A1, A3, Th65;

    end;

    begin

    definition

      let n be Nat, a,b be Point of ( TOP-REAL n);

      :: TOPREAL6:def1

      func dist (a,b) -> Real means

      : Def1: ex p,q be Point of ( Euclid n) st p = a & q = b & it = ( dist (p,q));

      existence

      proof

        reconsider p = a, q = b as Point of ( Euclid n) by TOPREAL3: 8;

        take ( dist (p,q));

        thus thesis;

      end;

      uniqueness ;

      commutativity ;

    end

    reserve r1,r2,s1,s2 for Real;

    theorem :: TOPREAL6:91

    

     Th84: for u,v be Point of ( Euclid 2) st u = |[r1, s1]| & v = |[r2, s2]| holds ( dist (u,v)) = ( sqrt (((r1 - r2) ^2 ) + ((s1 - s2) ^2 )))

    proof

      let u,v be Point of ( Euclid 2) such that

       A1: u = |[r1, s1]| and

       A2: v = |[r2, s2]|;

      

       A3: ( |[r1, s1]| `1 ) = r1 by EUCLID: 52;

      

       A4: ( |[r2, s2]| `2 ) = s2 by EUCLID: 52;

      

       A5: ( |[r2, s2]| `1 ) = r2 by EUCLID: 52;

      

       A6: ( |[r1, s1]| `2 ) = s1 by EUCLID: 52;

      

      thus ( dist (u,v)) = (( Pitag_dist 2) . (u,v)) by METRIC_1:def 1

      .= ( sqrt (((r1 - r2) ^2 ) + ((s1 - s2) ^2 ))) by A1, A2, A3, A6, A5, A4, TOPREAL3: 7;

    end;

    theorem :: TOPREAL6:92

    

     Th85: ( dist (p,q)) = ( sqrt ((((p `1 ) - (q `1 )) ^2 ) + (((p `2 ) - (q `2 )) ^2 )))

    proof

      

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

      

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

      ex a,b be Point of ( Euclid 2) st p = a & q = b & ( dist (a,b)) = ( dist (p,q)) by Def1;

      hence thesis by A1, A2, Th84;

    end;

    theorem :: TOPREAL6:93

    for p be Point of ( TOP-REAL n) holds ( dist (p,p)) = 0

    proof

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

      ex a,b be Point of ( Euclid n) st a = p & b = p & ( dist (a,b)) = ( dist (p,p)) by Def1;

      hence thesis by METRIC_1: 1;

    end;

    theorem :: TOPREAL6:94

    for p,q,r be Point of ( TOP-REAL n) holds ( dist (p,r)) <= (( dist (p,q)) + ( dist (q,r)))

    proof

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

      

       A1: ex a,b be Point of ( Euclid n) st a = p & b = r & ( dist (a,b)) = ( dist (p,r)) by Def1;

      

       A2: ex a,b be Point of ( Euclid n) st a = q & b = r & ( dist (a,b)) = ( dist (q,r)) by Def1;

      ex a,b be Point of ( Euclid n) st a = p & b = q & ( dist (a,b)) = ( dist (p,q)) by Def1;

      hence thesis by A1, A2, METRIC_1: 4;

    end;

    theorem :: TOPREAL6:95

    for x1,x2,y1,y2 be Real, a,b be Point of ( TOP-REAL 2) st x1 <= (a `1 ) & (a `1 ) <= x2 & y1 <= (a `2 ) & (a `2 ) <= y2 & x1 <= (b `1 ) & (b `1 ) <= x2 & y1 <= (b `2 ) & (b `2 ) <= y2 holds ( dist (a,b)) <= ((x2 - x1) + (y2 - y1))

    proof

      let x1,x2,y1,y2 be Real, a,b be Point of ( TOP-REAL 2) such that

       A1: x1 <= (a `1 ) and

       A2: (a `1 ) <= x2 and

       A3: y1 <= (a `2 ) and

       A4: (a `2 ) <= y2 and

       A5: x1 <= (b `1 ) and

       A6: (b `1 ) <= x2 and

       A7: y1 <= (b `2 ) and

       A8: (b `2 ) <= y2;

      

       A9: |.((a `2 ) - (b `2 )).| <= (y2 - y1) by A3, A4, A7, A8, JGRAPH_1: 27;

      

       A10: (((a `1 ) - (b `1 )) ^2 ) >= 0 by XREAL_1: 63;

      

       A11: (((a `2 ) - (b `2 )) ^2 ) >= 0 by XREAL_1: 63;

      ( dist (a,b)) = ( sqrt ((((a `1 ) - (b `1 )) ^2 ) + (((a `2 ) - (b `2 )) ^2 ))) by Th85;

      then ( dist (a,b)) <= (( sqrt (((a `1 ) - (b `1 )) ^2 )) + ( sqrt (((a `2 ) - (b `2 )) ^2 ))) by A10, A11, SQUARE_1: 59;

      then ( dist (a,b)) <= ( |.((a `1 ) - (b `1 )).| + ( sqrt (((a `2 ) - (b `2 )) ^2 ))) by COMPLEX1: 72;

      then

       A12: ( dist (a,b)) <= ( |.((a `1 ) - (b `1 )).| + |.((a `2 ) - (b `2 )).|) by COMPLEX1: 72;

       |.((a `1 ) - (b `1 )).| <= (x2 - x1) by A1, A2, A5, A6, JGRAPH_1: 27;

      then ( |.((a `1 ) - (b `1 )).| + |.((a `2 ) - (b `2 )).|) <= ((x2 - x1) + (y2 - y1)) by A9, XREAL_1: 7;

      hence thesis by A12, XXREAL_0: 2;

    end;