topreala.miz

    begin

    set R = the carrier of R^1 ;



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

    reserve i for Integer,

a,b,r,s for Real;

    registration

      let r be Real, s be positive Real;

      cluster ].r, (r + s).[ -> non empty;

      coherence

      proof

        (r + 0 ) < (r + s) by XREAL_1: 6;

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

        hence thesis by XXREAL_1: 4;

      end;

      cluster [.r, (r + s).[ -> non empty;

      coherence

      proof

        (r + 0 ) < (r + s) by XREAL_1: 6;

        hence thesis by XXREAL_1: 3;

      end;

      cluster ].r, (r + s).] -> non empty;

      coherence

      proof

        (r + 0 ) < (r + s) by XREAL_1: 6;

        hence thesis by XXREAL_1: 2;

      end;

      cluster [.r, (r + s).] -> non empty;

      coherence

      proof

        (r + 0 ) < (r + s) by XREAL_1: 6;

        hence thesis by XXREAL_1: 1;

      end;

      cluster ].(r - s), r.[ -> non empty;

      coherence

      proof

        (r - s) < (r - 0 ) by XREAL_1: 15;

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

        hence thesis by XXREAL_1: 4;

      end;

      cluster [.(r - s), r.[ -> non empty;

      coherence

      proof

        (r - s) < (r - 0 ) by XREAL_1: 15;

        hence thesis by XXREAL_1: 3;

      end;

      cluster ].(r - s), r.] -> non empty;

      coherence

      proof

        (r - s) < (r - 0 ) by XREAL_1: 15;

        hence thesis by XXREAL_1: 32;

      end;

      cluster [.(r - s), r.] -> non empty;

      coherence

      proof

        (r - s) < (r - 0 ) by XREAL_1: 15;

        hence thesis by XXREAL_1: 1;

      end;

    end

    registration

      let r be non positive Real, s be positive Real;

      cluster ].r, s.[ -> non empty;

      coherence

      proof

        r < ((r + s) / 2) & ((r + s) / 2) < s by XREAL_1: 226;

        hence thesis by XXREAL_1: 4;

      end;

      cluster [.r, s.[ -> non empty;

      coherence by XXREAL_1: 3;

      cluster ].r, s.] -> non empty;

      coherence by XXREAL_1: 2;

      cluster [.r, s.] -> non empty;

      coherence by XXREAL_1: 1;

    end

    registration

      let r be negative Real, s be non negative Real;

      cluster ].r, s.[ -> non empty;

      coherence

      proof

        r < ((r + s) / 2) & ((r + s) / 2) < s by XREAL_1: 226;

        hence thesis by XXREAL_1: 4;

      end;

      cluster [.r, s.[ -> non empty;

      coherence by XXREAL_1: 3;

      cluster ].r, s.] -> non empty;

      coherence by XXREAL_1: 2;

      cluster [.r, s.] -> non empty;

      coherence by XXREAL_1: 1;

    end

    begin

    theorem :: TOPREALA:1

    for f be Function, x,X be set st x in ( dom f) & (f . x) in (f .: X) & f is one-to-one holds x in X

    proof

      let f be Function, x,X be set;

      assume

       A1: x in ( dom f);

      assume (f . x) in (f .: X);

      then

       A2: ex a be object st a in ( dom f) & a in X & (f . x) = (f . a) by FUNCT_1:def 6;

      assume f is one-to-one;

      hence thesis by A1, A2, FUNCT_1:def 4;

    end;

    theorem :: TOPREALA:2

    for f be FinSequence, i be Nat st (i + 1) in ( dom f) holds i in ( dom f) or i = 0

    proof

      let f be FinSequence;

      let i be Nat;

      assume

       A1: (i + 1) in ( dom f);

      then 1 <= (i + 1) by FINSEQ_3: 25;

      then

       A2: 1 < (i + 1) or (1 + 0 ) = (i + 1) by XXREAL_0: 1;

      per cases by A2, NAT_1: 13;

        suppose i = 0 ;

        hence thesis;

      end;

        suppose

         A3: 1 <= i;

        (i + 1) <= ( len f) by A1, FINSEQ_3: 25;

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

        hence thesis by A3, FINSEQ_3: 25;

      end;

    end;

    theorem :: TOPREALA:3



     Th3: for x,y,X,Y be set, f be Function st x <> y & f in ( product ((x,y) --> (X,Y))) holds (f . x) in X & (f . y) in Y

    proof

      let x,y,X,Y be set, f be Function such that

       A1: x <> y and

       A2: f in ( product ((x,y) --> (X,Y)));

      set g = ((x,y) --> (X,Y));



       A3: ( dom g) = {x, y} by FUNCT_4: 62;

      then y in ( dom g) by TARSKI:def 2;

      then

       A4: (f . y) in (g . y) by A2, CARD_3: 9;

      x in ( dom g) by A3, TARSKI:def 2;

      then (f . x) in (g . x) by A2, CARD_3: 9;

      hence thesis by A1, A4, FUNCT_4: 63;

    end;

    theorem :: TOPREALA:4



     Th4: for a,b be object holds <*a, b*> = ((1,2) --> (a,b))

    proof

      let a,b be object;

      set f = ((1,2) --> (a,b));

      set g = <*a, b*>;



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

       A2:

      now

        let x be object;

        assume

         A3: x in ( dom f);

        per cases by A1, A3, TARSKI:def 2;

          suppose

           A4: x = 1;



          hence (f . x) = a by FUNCT_4: 63

          .= (g . x) by A4, FINSEQ_1: 44;

        end;

          suppose

           A5: x = 2;



          hence (f . x) = b by FUNCT_4: 63

          .= (g . x) by A5, FINSEQ_1: 44;

        end;

      end;

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

      hence thesis by A2, FUNCT_1: 2, FUNCT_4: 62;

    end;

    begin

    registration

      cluster constituted-FinSeqs non empty strict for TopSpace;

      existence

      proof

        take T = ( TopSpaceMetr ( Euclid 1));

        thus for a be Element of T holds a is FinSequence

        proof

          let a be Element of T;

          T = the TopStruct of ( TOP-REAL 1) by EUCLID:def 8;

          hence a is FinSequence;

        end;

        thus thesis;

      end;

    end

    registration

      let T be constituted-FinSeqs TopSpace;

      cluster -> constituted-FinSeqs for SubSpace of T;

      coherence

      proof

        let X be SubSpace of T;

        let p be Element of X;



         A1: the carrier of X is Subset of T by TSEP_1: 1;

        per cases ;

          suppose the carrier of X is non empty;

          then p in the carrier of X;

          then

          reconsider p as Point of T by A1;

          p is FinSequence;

          hence thesis;

        end;

          suppose the carrier of X is empty;

          hence thesis;

        end;

      end;

    end

    theorem :: TOPREALA:5



     Th5: for T be non empty TopSpace, Z be non empty SubSpace of T, t be Point of T, z be Point of Z, N be open a_neighborhood of t, M be Subset of Z st t = z & M = (N /\ ( [#] Z)) holds M is open a_neighborhood of z

    proof

      let T be non empty TopSpace, Z be non empty SubSpace of T, t be Point of T, z be Point of Z, N be open a_neighborhood of t, M be Subset of Z such that

       A1: t = z and

       A2: M = (N /\ ( [#] Z));

      M is open by A2, TOPS_2: 24;

      then

       A3: ( Int M) = M by TOPS_1: 23;

      t in ( Int N) & ( Int N) c= N by CONNSP_2:def 1, TOPS_1: 16;

      then z in ( Int M) by A1, A2, A3, XBOOLE_0:def 4;

      hence thesis by A2, CONNSP_2:def 1, TOPS_2: 24;

    end;

    registration

      cluster empty -> discrete anti-discrete for TopSpace;

      coherence

      proof

        let T be TopSpace;

        assume T is empty;

        then the carrier of T = {} ;

        then ( bool the carrier of T) = { {} , the carrier of T} by ENUMSET1: 29, ZFMISC_1: 1;

        hence thesis by TDLAT_3: 14;

      end;

    end

    registration

      let X be discrete TopSpace, Y be TopSpace;

      cluster -> continuous for Function of X, Y;

      coherence by TEX_2: 62;

    end

    theorem :: TOPREALA:6



     Th6: for X be TopSpace, Y be TopStruct, f be Function of X, Y st f is empty holds f is continuous

    proof

      let X be TopSpace, Y be TopStruct, f be Function of X, Y such that

       A1: f is empty;

      let P be Subset of Y;

      assume P is closed;

      (f " P) = ( {} X) by A1;

      hence thesis;

    end;

    registration

      let X be TopSpace, Y be TopStruct;

      cluster empty -> continuous for Function of X, Y;

      coherence by Th6;

    end

    theorem :: TOPREALA:7

    for X be TopStruct, Y be non empty TopStruct, Z be non empty SubSpace of Y, f be Function of X, Z holds f is Function of X, Y

    proof

      let X be TopStruct, Y be non empty TopStruct, Z be non empty SubSpace of Y;

      let f be Function of X, Z;

      the carrier of Z is Subset of Y by TSEP_1: 1;

      then

       A1: ( rng f) c= the carrier of Y by XBOOLE_1: 1;

      ( dom f) = the carrier of X by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_2: 2;

    end;

    theorem :: TOPREALA:8

    for S,T be non empty TopSpace, X be Subset of S, Y be Subset of T, f be continuous Function of S, T, g be Function of (S | X), (T | Y) st g = (f | X) holds g is continuous

    proof

      let S,T be non empty TopSpace, X be Subset of S, Y be Subset of T, f be continuous Function of S, T, g be Function of (S | X), (T | Y) such that

       A1: g = (f | X);

      set h = (f | X);



       A2: the carrier of (S | X) = X & ( rng h) c= the carrier of T by PRE_TOPC: 8;

      ( dom f) = the carrier of S by FUNCT_2:def 1;

      then ( dom h) = X by RELAT_1: 62;

      then

      reconsider h as Function of (S | X), T by A2, FUNCT_2: 2;

      h is continuous by TOPMETR: 7;

      hence thesis by A1, TOPMETR: 6;

    end;

    theorem :: TOPREALA:9

    for S,T be non empty TopSpace, Z be non empty SubSpace of T, f be Function of S, T, g be Function of S, Z st f = g & f is open holds g is open

    proof

      let S,T be non empty TopSpace, Z be non empty SubSpace of T, f be Function of S, T, g be Function of S, Z such that

       A1: f = g and

       A2: f is open;

      for p be Point of S, P be open a_neighborhood of p holds ex R be a_neighborhood of (g . p) st R c= (g .: P)

      proof

        let p be Point of S, P be open a_neighborhood of p;

        consider R be open a_neighborhood of (f . p) such that

         A3: R c= (f .: P) by A2, TOPGRP_1: 22;

        reconsider R2 = (R /\ ( [#] Z)) as Subset of Z;

        reconsider R2 as a_neighborhood of (g . p) by A1, Th5;

        take R2;

        R2 c= R by XBOOLE_1: 17;

        hence thesis by A1, A3;

      end;

      hence thesis by TOPGRP_1: 23;

    end;

    theorem :: TOPREALA:10

    for S,T be non empty TopSpace, S1 be Subset of S, T1 be Subset of T, f be Function of S, T, g be Function of (S | S1), (T | T1) st g = (f | S1) & g is onto & f is open one-to-one holds g is open

    proof

      let S,T be non empty TopSpace, S1 be Subset of S, T1 be Subset of T, f be Function of S, T, g be Function of (S | S1), (T | T1) such that

       A1: g = (f | S1) and

       A2: ( rng g) = the carrier of (T | T1) and

       A3: f is open and

       A4: f is one-to-one;

      let A be Subset of (S | S1);



       A5: ( [#] (T | T1)) = T1 by PRE_TOPC:def 5;

      assume A is open;

      then

      consider C be Subset of S such that

       A6: C is open and

       A7: (C /\ ( [#] (S | S1))) = A by TOPS_2: 24;



       A8: ( [#] (S | S1)) = S1 & (g .: (C /\ S1)) c= ((g .: C) /\ (g .: S1)) by PRE_TOPC:def 5, RELAT_1: 121;



       A9: (g .: A) = ((f .: C) /\ T1)

      proof

        (g .: C) c= (f .: C) by A1, RELAT_1: 128;

        then ((g .: C) /\ (g .: S1)) c= ((f .: C) /\ T1) by A5, XBOOLE_1: 27;

        hence (g .: A) c= ((f .: C) /\ T1) by A7, A8;

        let y be object;



         A10: ( dom g) c= ( dom f) & ( dom f) = the carrier of S by A1, FUNCT_2:def 1, RELAT_1: 60;

        assume

         A11: y in ((f .: C) /\ T1);

        then y in (f .: C) by XBOOLE_0:def 4;

        then

        consider x be Element of S such that

         A12: x in C and

         A13: y = (f . x) by FUNCT_2: 65;

        y in T1 by A11, XBOOLE_0:def 4;

        then

        consider a be object such that

         A14: a in ( dom g) and

         A15: (g . a) = y by A2, A5, FUNCT_1:def 3;

        (f . a) = (g . a) by A1, A14, FUNCT_1: 47;

        then a = x by A4, A13, A14, A15, A10, FUNCT_1:def 4;

        then a in A by A7, A12, A14, XBOOLE_0:def 4;

        hence thesis by A14, A15, FUNCT_1:def 6;

      end;

      (f .: C) is open by A3, A6;

      hence thesis by A5, A9, TOPS_2: 24;

    end;

    theorem :: TOPREALA:11

    for X,Y,Z be non empty TopSpace, f be Function of X, Y, g be Function of Y, Z st f is open & g is open holds (g * f) is open

    proof

      let X,Y,Z be non empty TopSpace, f be Function of X, Y, g be Function of Y, Z such that

       A1: f is open and

       A2: g is open;

      let A be Subset of X;

      assume A is open;

      then

       A3: (f .: A) is open by A1;

      ((g * f) .: A) = (g .: (f .: A)) by RELAT_1: 126;

      hence thesis by A2, A3;

    end;

    theorem :: TOPREALA:12

    for X,Y be TopSpace, Z be open SubSpace of Y, f be Function of X, Y, g be Function of X, Z st f = g & g is open holds f is open

    proof

      let X,Y be TopSpace, Z be open SubSpace of Y, f be Function of X, Y, g be Function of X, Z such that

       A1: f = g and

       A2: g is open;

      let A be Subset of X;

      assume A is open;

      then (g .: A) is open by A2;

      hence thesis by A1, TSEP_1: 17;

    end;

    theorem :: TOPREALA:13



     Th13: for S,T be non empty TopSpace, f be Function of S, T st f is one-to-one onto holds f is continuous iff (f " ) is open

    proof

      let S,T be non empty TopSpace, f be Function of S, T such that

       A1: f is one-to-one;

      assume f is onto;

      then

       A2: (f qua Function " ) = (f " ) by A1, TOPS_2:def 4;



       A3: ( [#] T) <> {} ;

      thus f is continuous implies (f " ) is open

      proof

        assume

         A4: f is continuous;

        let A be Subset of T;

        assume A is open;

        then (f " A) is open by A3, A4, TOPS_2: 43;

        hence thesis by A1, A2, FUNCT_1: 85;

      end;

      assume

       A5: (f " ) is open;

      now

        let A be Subset of T;

        assume A is open;

        then ((f " ) .: A) is open by A5;

        hence (f " A) is open by A1, A2, FUNCT_1: 85;

      end;

      hence thesis by A3, TOPS_2: 43;

    end;

    theorem :: TOPREALA:14

    for S,T be non empty TopSpace, f be Function of S, T st f is one-to-one onto holds f is open iff (f " ) is continuous

    proof

      let S,T be non empty TopSpace, f be Function of S, T such that

       A1: f is one-to-one;

      assume f is onto;

      then

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

      then ( rng (f " )) = ( [#] S) by A1, TOPS_2: 49;

      then

       A3: (f " ) is onto;

      (f " ) is one-to-one & ((f " ) " ) = f by A1, A2, TOPS_2: 50, TOPS_2: 51;

      hence thesis by A3, Th13;

    end;

    theorem :: TOPREALA:15

    for S be TopSpace, T be non empty TopSpace holds (S,T) are_homeomorphic iff ( the TopStruct of S, the TopStruct of T) are_homeomorphic

    proof

      let S be TopSpace, T be non empty TopSpace;

      set SS = the TopStruct of S;

      set TT = the TopStruct of T;



       A1: ( [#] S) = ( [#] SS) & ( [#] T) = ( [#] TT);

      thus (S,T) are_homeomorphic implies ( the TopStruct of S, the TopStruct of T) are_homeomorphic

      proof

        given f be Function of S, T such that

         A2: f is being_homeomorphism;

        reconsider g = f as Function of SS, TT;

         A3:

        now

          let P be Subset of SS;

          reconsider R = P as Subset of S;



          thus (g .: ( Cl P)) = (f .: ( Cl R)) by TOPS_3: 80

          .= ( Cl (f .: R)) by A2, TOPS_2: 60

          .= ( Cl (g .: P)) by TOPS_3: 80;

        end;

        take g;

        ( dom f) = ( [#] S) & ( rng f) = ( [#] T) by A2, TOPS_2: 60;

        hence thesis by A1, A2, A3, TOPS_2: 60;

      end;

      given f be Function of SS, TT such that

       A4: f is being_homeomorphism;

      reconsider g = f as Function of S, T;

       A5:

      now

        let P be Subset of S;

        reconsider R = P as Subset of SS;



        thus (g .: ( Cl P)) = (f .: ( Cl R)) by TOPS_3: 80

        .= ( Cl (f .: R)) by A4, TOPS_2: 60

        .= ( Cl (g .: P)) by TOPS_3: 80;

      end;

      take g;

      ( dom f) = ( [#] SS) & ( rng f) = ( [#] TT) by A4, TOPS_2: 60;

      hence thesis by A1, A4, A5, TOPS_2: 60;

    end;

    theorem :: TOPREALA:16

    for S,T be non empty TopSpace, f be Function of S, T st f is one-to-one onto continuous open holds f is being_homeomorphism

    proof

      let S,T be non empty TopSpace, f be Function of S, T such that

       A1: f is one-to-one and

       A2: f is onto and

       A3: f is continuous and

       A4: f is open;



       A5: ( [#] T) <> {} ;



       A6: ( dom f) = the carrier of S by FUNCT_2:def 1;



       A7: for P be Subset of S holds P is open iff (f .: P) is open

      proof

        let P be Subset of S;

        thus P is open implies (f .: P) is open by A4;

        assume (f .: P) is open;

        then (f " (f .: P)) is open by A3, A5, TOPS_2: 43;

        hence thesis by A1, A6, FUNCT_1: 94;

      end;

      ( dom f) = ( [#] S) & ( rng f) = ( [#] T) by A2, FUNCT_2:def 1;

      hence thesis by A1, A7, TOPGRP_1: 25;

    end;

    begin

    theorem :: TOPREALA:17

    for f be PartFunc of REAL , REAL st f = ( REAL --> r) holds (f | REAL ) is continuous

    proof

      let f be PartFunc of REAL , REAL such that

       A1: f = ( REAL --> r);

      (f | REAL ) is constant

      proof

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

        take r;

        let c be Element of REAL ;

        assume c in ( dom (f | REAL ));



        thus ((f | REAL ) . c) = (f . c)

        .= r by A1, FUNCOP_1: 7;

      end;

      hence thesis;

    end;

    theorem :: TOPREALA:18

    for f,f1,f2 be PartFunc of REAL , REAL st ( dom f) = (( dom f1) \/ ( dom f2)) & ( dom f1) is open & ( dom f2) is open & (f1 | ( dom f1)) is continuous & (f2 | ( dom f2)) is continuous & (for z be set st z in ( dom f1) holds (f . z) = (f1 . z)) & (for z be set st z in ( dom f2) holds (f . z) = (f2 . z)) holds (f | ( dom f)) is continuous

    proof

      let f,f1,f2 be PartFunc of REAL , REAL ;

      set X1 = ( dom f1), X2 = ( dom f2);

      assume that

       A1: ( dom f) = (X1 \/ X2) and

       A2: X1 is open and

       A3: X2 is open and

       A4: (f1 | X1) is continuous and

       A5: (f2 | X2) is continuous and

       A6: for z be set st z in X1 holds (f . z) = (f1 . z) and

       A7: for z be set st z in X2 holds (f . z) = (f2 . z);



       A8: (( dom f) /\ X1) = X1 by A1, XBOOLE_1: 7, XBOOLE_1: 28;



       A9: ( dom (f | X2)) = (( dom f) /\ X2) by RELAT_1: 61;

      let x be Real;

      assume x in ( dom (f | ( dom f)));

      then

       A10: x in ( dom f);



       A11: ((f | (X1 \/ X2)) . x) = (f . x) by A1;



       A12: (( dom f) /\ X2) = X2 by A1, XBOOLE_1: 7, XBOOLE_1: 28;



       A13: ( dom (f | X1)) = (( dom f) /\ X1) by RELAT_1: 61;

      per cases by A1, A10, XBOOLE_0:def 3;

        suppose

         A14: x in X1;



        then

         A15: ((f | (X1 \/ X2)) . x) = (f1 . x) by A6, A11

        .= ((f1 | X1) . x);

        for N1 be Neighbourhood of ((f | (X1 \/ X2)) . x) holds ex N be Neighbourhood of x st for x1 be Real st x1 in ( dom (f | (X1 \/ X2))) & x1 in N holds ((f | (X1 \/ X2)) . x1) in N1

        proof

          let N1 be Neighbourhood of ((f | (X1 \/ X2)) . x);

          consider N2 be Neighbourhood of x such that

           A16: N2 c= X1 by A2, A14, RCOMP_1: 18;

          x in ( dom (f1 | X1)) by A14;

          then (f1 | X1) is_continuous_in x by A4;

          then

          consider N be Neighbourhood of x such that

           A17: for x1 be Real st x1 in ( dom (f1 | X1)) & x1 in N holds ((f1 | X1) . x1) in N1 by A15, FCONT_1: 4;

          consider N3 be Neighbourhood of x such that

           A18: N3 c= N and

           A19: N3 c= N2 by RCOMP_1: 17;

          take N3;

          let x1 be Real such that

           A20: x1 in ( dom (f | (X1 \/ X2))) and

           A21: x1 in N3;

          per cases ;

            suppose

             A22: x1 in ( dom (f | X1));



             A23: ( dom (f | X1)) = (X1 /\ X1) by A1, A13, XBOOLE_1: 7, XBOOLE_1: 28

            .= ( dom (f1 | X1));



             A24: x1 in X1 by A13, A22, XBOOLE_0:def 4;

            ((f | (X1 \/ X2)) . x1) = (f . x1) by A20, FUNCT_1: 47

            .= (f1 . x1) by A6, A24

            .= ((f1 | X1) . x1);

            hence thesis by A17, A18, A21, A22, A23;

          end;

            suppose

             A25: not x1 in ( dom (f | X1));

            x1 in N2 by A19, A21;

            hence thesis by A13, A8, A16, A25;

          end;

        end;

        hence thesis by A1, FCONT_1: 4;

      end;

        suppose

         A26: x in X2;



        then

         A27: ((f | (X1 \/ X2)) . x) = (f2 . x) by A7, A11

        .= ((f2 | X2) . x);

        for N1 be Neighbourhood of ((f | (X1 \/ X2)) . x) holds ex N be Neighbourhood of x st for x1 be Real st x1 in ( dom (f | (X1 \/ X2))) & x1 in N holds ((f | (X1 \/ X2)) . x1) in N1

        proof

          let N1 be Neighbourhood of ((f | (X1 \/ X2)) . x);

          consider N2 be Neighbourhood of x such that

           A28: N2 c= X2 by A3, A26, RCOMP_1: 18;

          x in ( dom (f2 | X2)) by A26;

          then (f2 | X2) is_continuous_in x by A5;

          then

          consider N be Neighbourhood of x such that

           A29: for x1 be Real st x1 in ( dom (f2 | X2)) & x1 in N holds ((f2 | X2) . x1) in N1 by A27, FCONT_1: 4;

          consider N3 be Neighbourhood of x such that

           A30: N3 c= N and

           A31: N3 c= N2 by RCOMP_1: 17;

          take N3;

          let x1 be Real such that

           A32: x1 in ( dom (f | (X1 \/ X2))) and

           A33: x1 in N3;

          per cases ;

            suppose

             A34: x1 in ( dom (f | X2));



             A35: ( dom (f | X2)) = (X2 /\ X2) by A1, A9, XBOOLE_1: 7, XBOOLE_1: 28

            .= ( dom (f2 | X2));



             A36: x1 in X2 by A9, A34, XBOOLE_0:def 4;

            ((f | (X1 \/ X2)) . x1) = (f . x1) by A32, FUNCT_1: 47

            .= (f2 . x1) by A7, A36

            .= ((f2 | X2) . x1);

            hence thesis by A29, A30, A33, A34, A35;

          end;

            suppose

             A37: not x1 in ( dom (f | X2));

            x1 in N2 by A31, A33;

            hence thesis by A9, A12, A28, A37;

          end;

        end;

        hence thesis by A1, FCONT_1: 4;

      end;

    end;

    theorem :: TOPREALA:19



     Th19: for x be Point of R^1 , N be Subset of REAL , M be Subset of R^1 st M = N holds N is Neighbourhood of x implies M is a_neighborhood of x

    proof

      let x be Point of R^1 , N be Subset of REAL , M be Subset of R^1 such that

       A1: M = N;

      given r such that

       A2: 0 < r and

       A3: N = ].(x - r), (x + r).[;

      M is open by A1, A3, JORDAN6: 35;

      hence thesis by A1, A2, A3, CONNSP_2: 3, TOPREAL6: 15;

    end;

    theorem :: TOPREALA:20



     Th20: for x be Point of R^1 , M be a_neighborhood of x holds ex N be Neighbourhood of x st N c= M

    proof

      let x be Point of R^1 , M be a_neighborhood of x;

      consider V be Subset of R^1 such that

       A1: V is open and

       A2: V c= M and

       A3: x in V by CONNSP_2: 6;

      consider r be Real such that

       A4: r > 0 and

       A5: ].(x - r), (x + r).[ c= V by A1, A3, FRECHET: 8;

      reconsider N = ].(x - r), (x + r).[ as Neighbourhood of x by A4, RCOMP_1:def 6;

      take N;

      thus thesis by A2, A5;

    end;

    theorem :: TOPREALA:21



     Th21: for f be Function of R^1 , R^1 , g be PartFunc of REAL , REAL , x be Point of R^1 st f = g & g is_continuous_in x holds f is_continuous_at x

    proof

      let f be Function of R^1 , R^1 , g be PartFunc of REAL , REAL , x be Point of R^1 such that

       A1: f = g and

       A2: g is_continuous_in x;

      let G be a_neighborhood of (f . x);

      consider Z be Neighbourhood of (g . x) such that

       A3: Z c= G by A1, Th20;

      consider N be Neighbourhood of x such that

       A4: (g .: N) c= Z by A2, FCONT_1: 5;

      reconsider H = N as a_neighborhood of x by Th19, TOPMETR: 17;

      take H;

      thus thesis by A1, A3, A4;

    end;

    theorem :: TOPREALA:22

    for f be Function of R^1 , R^1 , g be Function of REAL , REAL st f = g & g is continuous holds f is continuous

    proof

      let f be Function of R^1 , R^1 , g be Function of REAL , REAL such that

       A1: f = g and

       A2: g is continuous;

      for x be Point of R^1 holds f is_continuous_at x

      proof

        let x be Point of R^1 ;

        ( dom f) = REAL by A1, FUNCT_2:def 1;

        then x in ( dom g) by A1;

        then g is_continuous_in x by A2;

        hence thesis by A1, Th21;

      end;

      hence thesis by TMAP_1: 44;

    end;

    theorem :: TOPREALA:23

    a <= r & s <= b implies [.r, s.] is closed Subset of ( Closed-Interval-TSpace (a,b))

    proof

      set T = ( Closed-Interval-TSpace (a,b));

      set A = [.r, s.];

      assume that

       A1: a <= r and

       A2: s <= b;

      per cases ;

        suppose r > s;

        then A = ( {} T) by XXREAL_1: 29;

        hence thesis;

      end;

        suppose r <= s;

        then a <= s by A1, XXREAL_0: 2;

        then the carrier of T = [.a, b.] by A2, TOPMETR: 18, XXREAL_0: 2;

        then

        reconsider A as Subset of T by A1, A2, XXREAL_1: 34;

        reconsider C = A as Subset of R^1 by TOPMETR: 17;

        C is closed & (C /\ ( [#] T)) = A by TREAL_1: 1, XBOOLE_1: 28;

        hence thesis by PRE_TOPC: 13;

      end;

    end;

    theorem :: TOPREALA:24

    a <= r & s <= b implies ].r, s.[ is open Subset of ( Closed-Interval-TSpace (a,b))

    proof

      set T = ( Closed-Interval-TSpace (a,b));

      set A = ].r, s.[;

      assume that

       A1: a <= r and

       A2: s <= b;

      per cases ;

        suppose r >= s;

        then A = ( {} T) by XXREAL_1: 28;

        hence thesis;

      end;

        suppose r < s;

        then a < s by A1, XXREAL_0: 2;

        then the carrier of T = [.a, b.] by A2, TOPMETR: 18, XXREAL_0: 2;

        then

        reconsider A as Subset of T by A1, A2, XXREAL_1: 37;

        reconsider C = A as Subset of R^1 by TOPMETR: 17;

        C is open & (C /\ ( [#] T)) = A by JORDAN6: 35, XBOOLE_1: 28;

        hence thesis by TOPS_2: 24;

      end;

    end;

    theorem :: TOPREALA:25

    a <= b & a <= r implies ].r, b.] is open Subset of ( Closed-Interval-TSpace (a,b))

    proof

      set T = ( Closed-Interval-TSpace (a,b));

      assume that

       A1: a <= b and

       A2: a <= r;



       A3: the carrier of T = [.a, b.] by A1, TOPMETR: 18;

      then

      reconsider A = ].r, b.] as Subset of T by A2, XXREAL_1: 36;

      reconsider C = ].r, (b + 1).[ as Subset of R^1 by TOPMETR: 17;



       A4: (C /\ ( [#] T)) c= A

      proof

        let x be object;

        assume

         A5: x in (C /\ ( [#] T));

        then

         A6: x in C by XBOOLE_0:def 4;

        then

        reconsider x as Real;



         A7: r < x by A6, XXREAL_1: 4;

        x <= b by A3, A5, XXREAL_1: 1;

        hence thesis by A7;

      end;

      (b + 0 ) < (b + 1) by XREAL_1: 6;

      then A c= C by XXREAL_1: 49;

      then A c= (C /\ ( [#] T)) by XBOOLE_1: 19;

      then C is open & (C /\ ( [#] T)) = A by A4, JORDAN6: 35;

      hence thesis by TOPS_2: 24;

    end;

    theorem :: TOPREALA:26

    a <= b & r <= b implies [.a, r.[ is open Subset of ( Closed-Interval-TSpace (a,b))

    proof

      set T = ( Closed-Interval-TSpace (a,b));

      assume that

       A1: a <= b and

       A2: r <= b;



       A3: the carrier of T = [.a, b.] by A1, TOPMETR: 18;

      then

      reconsider A = [.a, r.[ as Subset of T by A2, XXREAL_1: 35;

      reconsider C = ].(a - 1), r.[ as Subset of R^1 by TOPMETR: 17;



       A4: (C /\ ( [#] T)) c= A

      proof

        let x be object;

        assume

         A5: x in (C /\ ( [#] T));

        then

         A6: x in C by XBOOLE_0:def 4;

        then

        reconsider x as Real;



         A7: x < r by A6, XXREAL_1: 4;

        a <= x by A3, A5, XXREAL_1: 1;

        hence thesis by A7;

      end;

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

      then A c= C by XXREAL_1: 48;

      then A c= (C /\ ( [#] T)) by XBOOLE_1: 19;

      then C is open & (C /\ ( [#] T)) = A by A4, JORDAN6: 35;

      hence thesis by TOPS_2: 24;

    end;

    theorem :: TOPREALA:27



     Th27: a <= b & r <= s implies the carrier of [:( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (r,s)):] = [: [.a, b.], [.r, s.]:]

    proof

      set C1 = ( Closed-Interval-TSpace (a,b));

      set C2 = ( Closed-Interval-TSpace (r,s));

      assume a <= b & r <= s;

      then the carrier of C1 = [.a, b.] & the carrier of C2 = [.r, s.] by TOPMETR: 18;

      hence thesis by BORSUK_1:def 2;

    end;

    begin

    theorem :: TOPREALA:28

     |[a, b]| = ((1,2) --> (a,b)) by Th4;

    theorem :: TOPREALA:29

    ( |[a, b]| . 1) = a & ( |[a, b]| . 2) = b

    proof



      thus ( |[a, b]| . 1) = (((1,2) --> (a,b)) . 1) by Th4

      .= a by FUNCT_4: 63;



      thus ( |[a, b]| . 2) = (((1,2) --> (a,b)) . 2) by Th4

      .= b by FUNCT_4: 63;

    end;

    theorem :: TOPREALA:30



     Th30: ( closed_inside_of_rectangle (a,b,r,s)) = ( product ((1,2) --> ( [.a, b.], [.r, s.])))

    proof

      set A = [.a, b.], B = [.r, s.];

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

      set R = ( closed_inside_of_rectangle (a,b,r,s));



       A1: R = { p where p be Point of ( TOP-REAL 2) : a <= (p `1 ) & (p `1 ) <= b & r <= (p `2 ) & (p `2 ) <= s } by JGRAPH_6:def 2;

      thus R c= ( product f)

      proof

        let x be object;

        assume x in R;

        then

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

         A2: x = p and

         A3: a <= (p `1 ) & (p `1 ) <= b & r <= (p `2 ) & (p `2 ) <= s by A1;

         |[(p `1 ), (p `2 )]| = ((1,2) --> ((p `1 ),(p `2 ))) by Th4;

        then

         A4: p = ((1,2) --> ((p `1 ),(p `2 ))) by EUCLID: 53;

        (p `1 ) in A & (p `2 ) in B by A3;

        hence thesis by A2, A4, HILBERT3: 11;

      end;

      let x be object;

      assume

       A5: x in ( product f);

      then

      consider g be Function such that

       A6: x = g and

       A7: ( dom g) = ( dom f) and for y be object st y in ( dom f) holds (g . y) in (f . y) by CARD_3:def 5;



       A8: (g . 2) in B by A5, A6, Th3;



       A9: (g . 1) in A by A5, A6, Th3;

      then

      reconsider g1 = (g . 1), g2 = (g . 2) as Real by A8;



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

      then

      reconsider g as FinSequence by A7, FINSEQ_1: 2, FINSEQ_1:def 2;



       A11: ( len g) = 2 by A7, A10, FINSEQ_1: 2, FINSEQ_1:def 3;

       |[g1, g2]| = ((1,2) --> (g1,g2)) by Th4;

      then

      reconsider g as Point of ( TOP-REAL 2) by A11, FINSEQ_1: 44;



       A12: r <= (g `2 ) & (g `2 ) <= s by A8, XXREAL_1: 1;

      a <= (g `1 ) & (g `1 ) <= b by A9, XXREAL_1: 1;

      hence thesis by A1, A6, A12;

    end;

    theorem :: TOPREALA:31



     Th31: a <= b & r <= s implies |[a, r]| in ( closed_inside_of_rectangle (a,b,r,s))

    proof

      set o = |[a, r]|;



       A1: ( closed_inside_of_rectangle (a,b,r,s)) = { p where p be Point of ( TOP-REAL 2) : a <= (p `1 ) & (p `1 ) <= b & r <= (p `2 ) & (p `2 ) <= s } & (o `1 ) = a by EUCLID: 52, JGRAPH_6:def 2;



       A2: (o `2 ) = r by EUCLID: 52;

      assume a <= b & r <= s;

      hence thesis by A1, A2;

    end;

    definition

      let a,b,c,d be Real;

      :: TOPREALA:def1

      func Trectangle (a,b,c,d) -> SubSpace of ( TOP-REAL 2) equals (( TOP-REAL 2) | ( closed_inside_of_rectangle (a,b,c,d)));

      coherence ;

    end

    theorem :: TOPREALA:32



     Th32: a <= b & r <= s implies ( Trectangle (a,b,r,s)) is non empty

    proof

      assume a <= b & r <= s;

      then |[a, r]| in ( closed_inside_of_rectangle (a,b,r,s)) by Th31;

      hence the carrier of ( Trectangle (a,b,r,s)) is non empty;

    end;

    registration

      let a,c be non positive Real;

      let b,d be non negative Real;

      cluster ( Trectangle (a,b,c,d)) -> non empty;

      coherence by Th32;

    end

    definition

      :: TOPREALA:def2

      func R2Homeomorphism -> Function of [: R^1 , R^1 :], ( TOP-REAL 2) means

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

      existence by BORSUK_6: 20;

      uniqueness

      proof

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

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

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

        let a be Point of [: R^1 , R^1 :];

        consider x,y be Element of R such that

         A3: a = [x, y] by Lm1, DOMAIN_1: 1;



        thus (f . a) = <*x, y*> by A1, A3

        .= (g . a) by A2, A3;

      end;

    end

    theorem :: TOPREALA:33



     Th33: for A,B be Subset of REAL holds ( R2Homeomorphism .: [:A, B:]) = ( product ((1,2) --> (A,B)))

    proof

      for x,y be Real holds ( R2Homeomorphism . [x, y]) = <*x, y*> by Def2;

      hence thesis by TOPREAL6: 75;

    end;

    theorem :: TOPREALA:34



     Th34: R2Homeomorphism is being_homeomorphism

    proof

      for x,y be Real holds ( R2Homeomorphism . [x, y]) = <*x, y*> by Def2;

      hence thesis by TOPREAL6: 76;

    end;

    theorem :: TOPREALA:35



     Th35: a <= b & r <= s implies ( R2Homeomorphism | the carrier of [:( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (r,s)):]) is Function of [:( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (r,s)):], ( Trectangle (a,b,r,s))

    proof

      set C1 = ( Closed-Interval-TSpace (a,b));

      set C2 = ( Closed-Interval-TSpace (r,s));

      set TR = ( Trectangle (a,b,r,s));

      set h = ( R2Homeomorphism | the carrier of [:C1, C2:]);

      assume a <= b & r <= s;

      then

       A1: the carrier of [:C1, C2:] = [: [.a, b.], [.r, s.]:] by Th27;

      ( dom R2Homeomorphism ) = [:R, R:] by Lm1, FUNCT_2:def 1;

      then

       A2: ( dom h) = the carrier of [:C1, C2:] by A1, RELAT_1: 62, TOPMETR: 17, ZFMISC_1: 96;

      ( rng h) c= the carrier of TR

      proof

        let y be object;



         A3: the carrier of TR = ( closed_inside_of_rectangle (a,b,r,s)) & ( closed_inside_of_rectangle (a,b,r,s)) = { p where p be Point of ( TOP-REAL 2) : a <= (p `1 ) & (p `1 ) <= b & r <= (p `2 ) & (p `2 ) <= s } by JGRAPH_6:def 2, PRE_TOPC: 8;

        assume y in ( rng h);

        then

        consider x be object such that

         A4: x in ( dom h) and

         A5: (h . x) = y by FUNCT_1:def 3;

        reconsider x as Point of [: R^1 , R^1 :] by A4;

        ( dom h) c= [:R, R:] by A1, A2, TOPMETR: 17, ZFMISC_1: 96;

        then

        consider x1,x2 be Element of R such that

         A6: x = [x1, x2] by A4, DOMAIN_1: 1;



         A7: x2 in [.r, s.] by A1, A2, A4, A6, ZFMISC_1: 87;



         A8: (h . x) = ( R2Homeomorphism . x) by A4, FUNCT_1: 47;

        then

        reconsider p = (h . x) as Point of ( TOP-REAL 2);



         A9: (h . x) = <*x1, x2*> by A8, A6, Def2;

        then x2 = (p `2 ) by FINSEQ_1: 44;

        then

         A10: r <= (p `2 ) & (p `2 ) <= s by A7, XXREAL_1: 1;



         A11: x1 in [.a, b.] by A1, A2, A4, A6, ZFMISC_1: 87;

        x1 = (p `1 ) by A9, FINSEQ_1: 44;

        then a <= (p `1 ) & (p `1 ) <= b by A11, XXREAL_1: 1;

        hence thesis by A5, A3, A10;

      end;

      hence thesis by A2, FUNCT_2: 2;

    end;

    theorem :: TOPREALA:36



     Th36: a <= b & r <= s implies for h be Function of [:( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (r,s)):], ( Trectangle (a,b,r,s)) st h = ( R2Homeomorphism | the carrier of [:( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (r,s)):]) holds h is being_homeomorphism

    proof

      assume

       A1: a <= b & r <= s;

      set TR = ( Trectangle (a,b,r,s));



       A2: ( closed_inside_of_rectangle (a,b,r,s)) = { p where p be Point of ( TOP-REAL 2) : a <= (p `1 ) & (p `1 ) <= b & r <= (p `2 ) & (p `2 ) <= s } by JGRAPH_6:def 2;

      set p = |[a, r]|;

      (p `1 ) = a & (p `2 ) = r by EUCLID: 52;

      then p in ( closed_inside_of_rectangle (a,b,r,s)) by A1, A2;

      then

      reconsider T0 = TR as non empty SubSpace of ( TOP-REAL 2);

      set C2 = ( Closed-Interval-TSpace (r,s));

      set C1 = ( Closed-Interval-TSpace (a,b));

      let h be Function of [:C1, C2:], TR such that

       A3: h = ( R2Homeomorphism | the carrier of [:C1, C2:]);

      reconsider S0 = [:C1, C2:] as non empty SubSpace of [: R^1 , R^1 :] by BORSUK_3: 21;

      reconsider g = h as Function of S0, T0;



       A4: the carrier of TR = ( closed_inside_of_rectangle (a,b,r,s)) by PRE_TOPC: 8;



       A5: g is onto

      proof

        thus ( rng g) c= the carrier of T0;

        let y be object;



         A6: the carrier of [:C1, C2:] = [: [.a, b.], [.r, s.]:] & ( dom g) = the carrier of S0 by A1, Th27, FUNCT_2:def 1;

        assume y in the carrier of T0;

        then

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

         A7: y = p and

         A8: a <= (p `1 ) & (p `1 ) <= b & r <= (p `2 ) & (p `2 ) <= s by A2, A4;

        (p `1 ) in [.a, b.] & (p `2 ) in [.r, s.] by A8;

        then

         A9: [(p `1 ), (p `2 )] in ( dom g) by A6, ZFMISC_1:def 2;



        then (g . [(p `1 ), (p `2 )]) = ( R2Homeomorphism . [(p `1 ), (p `2 )]) by A3, FUNCT_1: 49

        .= |[(p `1 ), (p `2 )]| by Def2

        .= y by A7, EUCLID: 53;

        hence thesis by A9, FUNCT_1:def 3;

      end;

      g = ( R2Homeomorphism | S0) by A3;

      hence thesis by A5, Th34, JORDAN16: 9;

    end;

    theorem :: TOPREALA:37

    a <= b & r <= s implies ( [:( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (r,s)):],( Trectangle (a,b,r,s))) are_homeomorphic

    proof

      set C1 = ( Closed-Interval-TSpace (a,b));

      set C2 = ( Closed-Interval-TSpace (r,s));

      assume

       A1: a <= b & r <= s;

      then

      reconsider h = ( R2Homeomorphism | the carrier of [:C1, C2:]) as Function of [:C1, C2:], ( Trectangle (a,b,r,s)) by Th35;

      take h;

      thus thesis by A1, Th36;

    end;

    theorem :: TOPREALA:38



     Th38: a <= b & r <= s implies for A be Subset of ( Closed-Interval-TSpace (a,b)), B be Subset of ( Closed-Interval-TSpace (r,s)) holds ( product ((1,2) --> (A,B))) is Subset of ( Trectangle (a,b,r,s))

    proof

      set T = ( Closed-Interval-TSpace (a,b));

      set S = ( Closed-Interval-TSpace (r,s));

      assume a <= b & r <= s;

      then

       A1: the carrier of T = [.a, b.] & the carrier of S = [.r, s.] by TOPMETR: 18;

      let A be Subset of T;

      let B be Subset of S;

      ( closed_inside_of_rectangle (a,b,r,s)) = ( product ((1,2) --> ( [.a, b.], [.r, s.]))) by Th30;

      then ( product ((1,2) --> (A,B))) c= ( closed_inside_of_rectangle (a,b,r,s)) by A1, TOPREAL6: 21;

      hence thesis by PRE_TOPC: 8;

    end;

    theorem :: TOPREALA:39

    a <= b & r <= s implies for A be open Subset of ( Closed-Interval-TSpace (a,b)), B be open Subset of ( Closed-Interval-TSpace (r,s)) holds ( product ((1,2) --> (A,B))) is open Subset of ( Trectangle (a,b,r,s))

    proof

      set T = ( Closed-Interval-TSpace (a,b));

      set S = ( Closed-Interval-TSpace (r,s));

      assume

       A1: a <= b & r <= s;

      then

      reconsider h = ( R2Homeomorphism | the carrier of [:( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (r,s)):]) as Function of [:( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (r,s)):], ( Trectangle (a,b,r,s)) by Th35;

      let A be open Subset of T, B be open Subset of S;

      reconsider P = ( product ((1,2) --> (A,B))) as Subset of ( Trectangle (a,b,r,s)) by A1, Th38;



       A2: [:A, B:] is open by BORSUK_1: 6;

      the carrier of S is Subset of R^1 by TSEP_1: 1;

      then

       A3: B is Subset of REAL by TOPMETR: 17, XBOOLE_1: 1;

      the carrier of T is Subset of R^1 by TSEP_1: 1;

      then

       A4: A is Subset of REAL by TOPMETR: 17, XBOOLE_1: 1;



       A5: (h .: [:A, B:]) = ( R2Homeomorphism .: [:A, B:]) by RELAT_1: 129

      .= P by A4, A3, Th33;

      h is being_homeomorphism & ( Trectangle (a,b,r,s)) is non empty by A1, Th32, Th36;

      hence thesis by A5, A2, TOPGRP_1: 25;

    end;

    theorem :: TOPREALA:40

    a <= b & r <= s implies for A be closed Subset of ( Closed-Interval-TSpace (a,b)), B be closed Subset of ( Closed-Interval-TSpace (r,s)) holds ( product ((1,2) --> (A,B))) is closed Subset of ( Trectangle (a,b,r,s))

    proof

      set T = ( Closed-Interval-TSpace (a,b));

      set S = ( Closed-Interval-TSpace (r,s));

      assume

       A1: a <= b & r <= s;

      then

      reconsider h = ( R2Homeomorphism | the carrier of [:( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (r,s)):]) as Function of [:( Closed-Interval-TSpace (a,b)), ( Closed-Interval-TSpace (r,s)):], ( Trectangle (a,b,r,s)) by Th35;

      let A be closed Subset of T, B be closed Subset of S;

      reconsider P = ( product ((1,2) --> (A,B))) as Subset of ( Trectangle (a,b,r,s)) by A1, Th38;



       A2: [:A, B:] is closed by TOPALG_3: 15;

      the carrier of S is Subset of R^1 by TSEP_1: 1;

      then

       A3: B is Subset of REAL by TOPMETR: 17, XBOOLE_1: 1;

      the carrier of T is Subset of R^1 by TSEP_1: 1;

      then

       A4: A is Subset of REAL by TOPMETR: 17, XBOOLE_1: 1;



       A5: (h .: [:A, B:]) = ( R2Homeomorphism .: [:A, B:]) by RELAT_1: 129

      .= P by A4, A3, Th33;

      h is being_homeomorphism & ( Trectangle (a,b,r,s)) is non empty by A1, Th32, Th36;

      hence thesis by A5, A2, TOPS_2: 58;

    end;