mfold_0.miz



    begin

    reserve n,m for Nat,

p,q for Point of ( TOP-REAL n),

r for Real;

    theorem :: MFOLD_0:1

    

     Th1: for T be non empty TopSpace holds (T,(T | ( [#] T))) are_homeomorphic

    proof

      let X be non empty TopSpace;

      set f = ( id X);

      

       A1: ( dom f) = ( [#] X);

      

       A2: ( [#] (X | ( [#] X))) = ( [#] X) by PRE_TOPC:def 5;

      

       A3: ( rng f) = ( [#] (X | ( [#] X))) by PRE_TOPC:def 5;

      reconsider XX = (X | ( [#] X)) as non empty TopSpace;

      reconsider f as Function of X, XX by A2;

      

       ZZ: for P be Subset of X st P is closed holds ((f " ) " P) is closed

      proof

        let P be Subset of X;

        assume P is closed;

        then

         A4: (( [#] X) \ P) in the topology of X by PRE_TOPC:def 2, PRE_TOPC:def 3;

        

         A5: for x be object holds x in ((f " ) " P) iff x in P

        proof

          let x be object;

          hereby

            assume

             A6: x in ((f " ) " P);

            x in (f .: P) by A6, A3, TOPS_2: 54;

            then

            consider y be object such that

             A7: [y, x] in f & y in P by RELAT_1:def 13;

            thus x in P by A7, RELAT_1:def 10;

          end;

          assume

           A8: x in P;

          then [x, x] in ( id X) by RELAT_1:def 10;

          then x in (f .: P) by A8, RELAT_1:def 13;

          hence x in ((f " ) " P) by A3, TOPS_2: 54;

        end;

        

         S1: (( [#] X) \ P) = (( [#] (X | ( [#] X))) \ ((f " ) " P)) by A2, A5, TARSKI: 2;

        (( [#] X) \ P) = ((( [#] X) /\ ( [#] X)) \ P)

        .= ((( [#] X) \ P) /\ ( [#] X)) by XBOOLE_1: 49;

        then (( [#] X) \ P) in the topology of (X | ( [#] X)) by PRE_TOPC:def 4, A2, A4;

        then (( [#] (X | ( [#] X))) \ ((f " ) " P)) is open by PRE_TOPC:def 2, S1;

        hence ((f " ) " P) is closed by PRE_TOPC:def 3;

      end;

      

       S0: f is continuous by JGRAPH_1: 45;

      (f " ) is continuous by PRE_TOPC:def 6, ZZ;

      then f is being_homeomorphism by A1, A3, TOPS_2:def 5, S0;

      hence thesis by T_0TOPSP:def 1;

    end;

    definition

      let n, p, r;

      :: MFOLD_0:def1

      func Tball (p,r) -> SubSpace of ( TOP-REAL n) equals (( TOP-REAL n) | ( Ball (p,r)));

      correctness ;

    end

    registration

      let n, p;

      let s be positive Real;

      cluster ( Tball (p,s)) -> non empty;

      correctness ;

    end

    theorem :: MFOLD_0:2

    the carrier of ( Tball (p,r)) = ( Ball (p,r))

    proof

      ( [#] ( Tball (p,r))) = ( Ball (p,r)) by PRE_TOPC:def 5;

      hence thesis;

    end;

    theorem :: MFOLD_0:3

    

     Th3: for r,s be positive Real holds (( Tball (p,r)),( Tball (q,s))) are_homeomorphic

    proof

      set TR = ( TOP-REAL n);

      let r,s be positive Real;

      ( Ball (q,s)) c= ( Int ( cl_Ball (q,s))) by TOPREAL9: 16, TOPS_1: 24;

      then

       A2: ( cl_Ball (q,s)) is non boundary compact;

      ( Ball (p,r)) c= ( Int ( cl_Ball (p,r))) by TOPREAL9: 16, TOPS_1: 24;

      then ( cl_Ball (p,r)) is non boundary compact;

      then

      consider h be Function of (TR | ( cl_Ball (p,r))), (TR | ( cl_Ball (q,s))) such that

       A4: h is being_homeomorphism & (h .: ( Fr ( cl_Ball (p,r)))) = ( Fr ( cl_Ball (q,s))) by A2, BROUWER2: 7;

      

       A5: ( [#] (TR | ( cl_Ball (q,s)))) = ( cl_Ball (q,s)) by PRE_TOPC:def 5;

      

       A6: (h .: ( dom h)) = ( rng h) by RELAT_1: 113

      .= ( [#] (TR | ( cl_Ball (q,s)))) by FUNCT_2:def 3, A4;

      

       A7: ( Fr ( cl_Ball (p,r))) = ( Sphere (p,r)) by BROUWER2: 5;

      

       A8: ( [#] (TR | ( cl_Ball (p,r)))) = ( cl_Ball (p,r)) by PRE_TOPC:def 5;

      

       A9: (( Ball (q,s)) \/ ( Sphere (q,s))) = ( cl_Ball (q,s)) & ( Ball (q,s)) misses ( Sphere (q,s)) by TOPREAL9: 18, TOPREAL9: 19;

      

       A10: (( Ball (p,r)) \/ ( Sphere (p,r))) = ( cl_Ball (p,r)) & ( Ball (p,r)) misses ( Sphere (p,r)) by TOPREAL9: 18, TOPREAL9: 19;

      reconsider Br = ( Ball (p,r)) as Subset of (TR | ( cl_Ball (p,r))) by A10, A8, XBOOLE_1: 7;

      reconsider Bs = ( Ball (q,s)) as Subset of (TR | ( cl_Ball (q,s))) by A9, A5, XBOOLE_1: 7;

      

       A12: ( dom h) = ( [#] (TR | ( cl_Ball (p,r)))) by FUNCT_2:def 1;

      

       A13: (( Ball (q,s)) \/ ( Sphere (q,s))) = ( cl_Ball (q,s)) & ( Ball (q,s)) misses ( Sphere (q,s)) by TOPREAL9: 18, TOPREAL9: 19;

      

       A14: (( Ball (p,r)) \/ ( Sphere (p,r))) = ( cl_Ball (p,r)) & ( Ball (p,r)) misses ( Sphere (p,r)) by TOPREAL9: 18, TOPREAL9: 19;

      (( dom h) \ ( Sphere (p,r))) = ( Ball (p,r)) by A12, A8, XBOOLE_1: 88, A14;

      

      then (h .: Br) = ((h .: ( dom h)) \ ( Fr ( cl_Ball (q,s)))) by A4, FUNCT_1: 64, A7

      .= (( cl_Ball (q,s)) \ ( Sphere (q,s))) by BROUWER2: 5, A6, A5

      .= Bs by A13, XBOOLE_1: 88;

      then (((TR | ( cl_Ball (p,r))) | Br),((TR | ( cl_Ball (q,s))) | Bs)) are_homeomorphic by A4, METRIZTS: 3, METRIZTS:def 1;

      then ((TR | ( Ball (p,r))),((TR | ( cl_Ball (q,s))) | Bs)) are_homeomorphic by PRE_TOPC: 7, A8;

      hence thesis by PRE_TOPC: 7, A5;

    end;

    registration

      let n;

      cluster ( TOP-REAL n) -> second-countable;

      correctness

      proof

        set TR = ( TOP-REAL n), T = the TopStruct of TR;

        T = (TR | ( [#] TR)) by TSEP_1: 93;

        then ( weight T) = ( weight TR) by Th1, METRIZTS: 4;

        hence thesis by WAYBEL23:def 6;

      end;

    end

    

     Lm1: for p,q be Point of ( TOP-REAL n) holds for r,s be real number st r > 0 & s > 0 holds (( Tdisk (p,r)),( Tdisk (q,s))) are_homeomorphic

    proof

      set TR = ( TOP-REAL n);

      let p,q be Point of TR;

      let r,s be real number;

      assume that

       A1: r > 0 and

       A2: s > 0 ;

      ( Ball (q,s)) c= ( Int ( cl_Ball (q,s))) by TOPREAL9: 16, TOPS_1: 24;

      then

       A3: ( cl_Ball (q,s)) is non boundary compact by A2;

      ( Ball (p,r)) c= ( Int ( cl_Ball (p,r))) by TOPREAL9: 16, TOPS_1: 24;

      then ( cl_Ball (p,r)) is non boundary compact by A1;

      then ex h be Function of (TR | ( cl_Ball (p,r))), (TR | ( cl_Ball (q,s))) st h is being_homeomorphism & (h .: ( Fr ( cl_Ball (p,r)))) = ( Fr ( cl_Ball (q,s))) by A3, BROUWER2: 7;

      hence thesis by T_0TOPSP:def 1;

    end;

    theorem :: MFOLD_0:4

    for M be non empty TopSpace holds for q be Point of M, r be real number, p be Point of ( TOP-REAL n) st r > 0 holds for U be a_neighborhood of q st ((M | U),( Tball (p,r))) are_homeomorphic holds ex W be a_neighborhood of q st W c= ( Int U) & ((M | W),( Tdisk (p,r))) are_homeomorphic

    proof

      let M be non empty TopSpace;

      set TR = ( TOP-REAL n);

      let q be Point of M, r be real number, p be Point of TR such that

       A1: r > 0 ;

      let U be a_neighborhood of q such that

       A2: ((M | U),( Tball (p,r))) are_homeomorphic ;

      

       A3: ( [#] (M | U)) = U by PRE_TOPC:def 5;

      then

      reconsider IU = ( Int U) as Subset of (M | U) by TOPS_1: 16;

      set MU = (M | U);

      consider h be Function of MU, ( Tball (p,r)) such that

       A4: h is being_homeomorphism by T_0TOPSP:def 1, A2;

      

       A5: ( dom h) = ( [#] (M | U)) by A4, TOPS_2:def 5;

      

       A7: ( [#] ( Tball (p,r))) = ( Ball (p,r)) by PRE_TOPC:def 5;

      then

      reconsider W = (h .: IU) as Subset of TR by XBOOLE_1: 1;

      IU is open by TSEP_1: 9;

      then (h .: IU) is open by A4, TOPGRP_1: 25, A1;

      then

      reconsider W as open Subset of TR by A7, TSEP_1: 9;

      q in ( Int U) by CONNSP_2:def 1;

      then

       A8: (h . q) in W by A5, FUNCT_1:def 6;

      then

      reconsider hq = (h . q) as Point of TR;

      reconsider HQ = hq as Point of ( Euclid n) by EUCLID: 67;

      ( Int W) = W by TOPS_1: 23;

      then

      consider s be Real such that

       A9: s > 0 and

       A10: ( Ball (HQ,s)) c= W by A8, GOBOARD6: 5;

      set m = (s / 2);

      

       A11: ( Ball (HQ,s)) = ( Ball (hq,s)) by TOPREAL9: 13;

      set CL = ( cl_Ball (hq,m));

      

       A12: n in NAT by ORDINAL1:def 12;

      

       A13: CL c= ( Ball (hq,s)) by A9, A12, XREAL_1: 216, JORDAN: 21;

      then CL c= W by A10, A11;

      then

       A14: CL c= ( Ball (p,r)) by A7, XBOOLE_1: 1;

      set BB = ( Ball (hq,m));

      

       A15: BB c= CL by TOPREAL9: 16;

      then

      reconsider CL, BB as Subset of ( Tball (p,r)) by A14, XBOOLE_1: 1, A7;

      

       A16: ( rng h) = ( [#] ( Tball (p,r))) by A4, TOPS_2:def 5;

      

       A17: q in ( Int U) by CONNSP_2:def 1;

      

       A18: ( Int U) c= U by TOPS_1: 16;

      reconsider hBB = (h " BB) as Subset of M by A3, XBOOLE_1: 1;

      hq is Element of ( REAL n) by EUCLID: 22;

      then |.(hq - hq).| = 0 ;

      then hq in BB by A9;

      then

       A19: q in hBB by FUNCT_1:def 7, A5, A18, A17, A3;

      

       A20: ( dom h) = ( [#] MU) by A4, TOPS_2:def 5;

      

       A21: (h " W) = IU by FUNCT_1: 82, A4, FUNCT_1: 76, A20;

      CL meets ( Ball (p,r)) by A9, A7, XBOOLE_1: 67;

      then

      reconsider hCL = (h " CL) as non empty Subset of MU by A7, RELAT_1: 138, A16;

      

       A22: (h .: hCL) = CL by FUNCT_1: 77, A16;

      

       A23: (( Tball (p,r)) | CL) = (TR | ( cl_Ball (hq,m))) by A7, PRE_TOPC: 7;

      then

      reconsider HH = (h | hCL) as Function of (MU | hCL), ( Tdisk (hq,m)) by A22, A1, JORDAN24: 12;

      HH is being_homeomorphism by A22, A23, A4, METRIZTS: 2;

      then

       A24: ((MU | hCL),( Tdisk (hq,m))) are_homeomorphic by T_0TOPSP:def 1;

      (( Tdisk (hq,m)),( Tdisk (p,r))) are_homeomorphic by A1, A9, Lm1;

      then

       A25: ((MU | hCL),( Tdisk (p,r))) are_homeomorphic by A1, A9, BORSUK_3: 3, A24;

      reconsider HCL = hCL as Subset of M by A3, XBOOLE_1: 1;

      

       A26: (MU | hCL) = (M | HCL) by PRE_TOPC: 7, A3;

      BB c= W by A10, A11, A13, A15;

      then

       A27: (h " BB) c= (h " W) by RELAT_1: 143;

      BB is open by TSEP_1: 9;

      then (h " BB) is open by A4, TOPGRP_1: 26, A1;

      then hBB is open by A21, A27, TSEP_1: 9;

      then q in ( Int HCL) by RELAT_1: 143, A15, A19, TOPS_1: 22;

      then

       A28: HCL is a_neighborhood of q by CONNSP_2:def 1;

      CL c= W by A13, A10, A11;

      hence thesis by A28, RELAT_1: 143, A21, A25, A26;

    end;

    begin

    reserve M,M1,M2 for non empty TopSpace;

    definition

      let M;

      :: MFOLD_0:def2

      attr M is locally_euclidean means

      : Def2: for p be Point of M holds ex U be a_neighborhood of p, n st ((M | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

    end

    definition

      let n, M;

      :: MFOLD_0:def3

      attr M is n -locally_euclidean means

      : Def3: for p be Point of M holds ex U be a_neighborhood of p st ((M | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

    end

    registration

      let n;

      cluster ( Tdisk (( 0. ( TOP-REAL n)),1)) -> n -locally_euclidean;

      coherence

      proof

        let p be Point of ( Tdisk (( 0. ( TOP-REAL n)),1));

        ( Int ( [#] ( Tdisk (( 0. ( TOP-REAL n)),1)))) = ( [#] ( Tdisk (( 0. ( TOP-REAL n)),1))) by TOPS_1: 15;

        then

        reconsider CM = ( [#] ( Tdisk (( 0. ( TOP-REAL n)),1))) as non empty a_neighborhood of p by CONNSP_2:def 1;

        take CM;

        thus thesis by TSEP_1: 93;

      end;

    end

    registration

      let n;

      cluster n -locally_euclidean for non empty TopSpace;

      existence

      proof

        take M = ( Tdisk (( 0. ( TOP-REAL n)),1));

        thus thesis;

      end;

    end

    registration

      let n;

      cluster n -locally_euclidean -> locally_euclidean for non empty TopSpace;

      coherence

      proof

        let M be non empty TopSpace;

        assume

         A1: M is n -locally_euclidean;

        let p be Point of M;

        ex U be a_neighborhood of p st ((M | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A1;

        hence thesis;

      end;

    end

    begin

    definition

      let M be non empty TopSpace;

      :: MFOLD_0:def4

      func Int M -> Subset of M means

      : Def4: for p be Point of M holds p in it iff ex U be a_neighborhood of p, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

      existence

      proof

        set I = { p where p be Point of M : ex U be a_neighborhood of p, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic };

        I c= the carrier of M

        proof

          let x be object;

          assume x in I;

          then ex q be Point of M st x = q & ex U be a_neighborhood of q, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

          hence thesis;

        end;

        then

        reconsider I as Subset of M;

        take I;

        let p be Point of M;

        hereby

          assume p in I;

          then ex q be Point of M st p = q & ex U be a_neighborhood of q, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

          hence ex U be a_neighborhood of p, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let I1,I2 be Subset of M such that

         A1: for p be Point of M holds p in I1 iff ex U be a_neighborhood of p, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic and

         A2: for p be Point of M holds p in I2 iff ex U be a_neighborhood of p, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

        hereby

          let x be object;

          assume

           A3: x in I1;

          then

          reconsider p = x as Point of M;

          ex U be a_neighborhood of p, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A3, A1;

          hence x in I2 by A2;

        end;

        let x be object;

        assume

         A4: x in I2;

        then

        reconsider p = x as Point of M;

        ex U be a_neighborhood of p, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A4, A2;

        hence x in I1 by A1;

      end;

    end

    registration

      let M be locally_euclidean non empty TopSpace;

      cluster ( Int M) -> non empty open;

      coherence

      proof

        

         A1: for x be set holds x in ( Int M) iff ex U be Subset of M st U is open & U c= ( Int M) & x in U

        proof

          let x be set;

          hereby

            assume

             A2: x in ( Int M);

            then

            reconsider p = x as Point of M;

            consider U be a_neighborhood of p, n such that

             A3: ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A2, Def4;

            take W = ( Int U);

            W c= ( Int M)

            proof

              let y be object;

              assume

               A4: y in W;

              then

              reconsider q = y as Point of M;

              U is a_neighborhood of q by A4, CONNSP_2:def 1;

              hence thesis by Def4, A3;

            end;

            hence W is open & W c= ( Int M) & x in W by CONNSP_2:def 1;

          end;

          thus thesis;

        end;

        set p = the Point of M;

        consider U be a_neighborhood of p, n such that

         A5: ((M | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Def2;

        

         A6: ( [#] (M | U)) = U by PRE_TOPC:def 5;

        then

        reconsider IU = ( Int U) as Subset of (M | U) by TOPS_1: 16;

        set MU = (M | U);

        set TR = ( TOP-REAL n);

        consider h be Function of MU, ( Tdisk (( 0. TR),1)) such that

         A7: h is being_homeomorphism by T_0TOPSP:def 1, A5;

        IU is open by TSEP_1: 9;

        then (h .: IU) is open by A7, TOPGRP_1: 25;

        then (h .: IU) in the topology of ( Tdisk (( 0. TR),1)) by PRE_TOPC:def 2;

        then

        consider W be Subset of TR such that

         A8: W in the topology of TR and

         A9: (h .: IU) = (W /\ ( [#] ( Tdisk (( 0. TR),1)))) by PRE_TOPC:def 4;

        

         A10: ( [#] ( Tdisk (( 0. TR),1))) = ( cl_Ball (( 0. TR),1)) by PRE_TOPC:def 5;

        

         A11: ( dom h) = ( [#] MU) by A7, TOPS_2:def 5;

        

         A12: ( Ball (( 0. TR),1)) c= ( cl_Ball (( 0. TR),1)) by TOPREAL9: 16;

        reconsider W as open Subset of TR by A8, PRE_TOPC:def 2;

        set WB = (W /\ ( Ball (( 0. TR),1)));

        p in ( Int U) by CONNSP_2:def 1;

        then

         A13: (h . p) in (h .: IU) by A11, FUNCT_1:def 6;

        then

         A14: (h . p) in W by A9, XBOOLE_0:def 4;

        then

        reconsider hp = (h . p) as Point of TR;

        

         A15: (h .: IU) = (W /\ ( cl_Ball (( 0. TR),1))) by PRE_TOPC:def 5, A9;

        WB is non empty

        proof

          reconsider HP = hp as Point of ( Euclid n) by EUCLID: 67;

          

           A16: ( Ball (( 0. TR),1)) misses ( Sphere (( 0. TR),1)) by TOPREAL9: 19;

          

           A17: ( cl_Ball (( 0. TR),1)) = (( Ball (( 0. TR),1)) \/ ( Sphere (( 0. TR),1))) by TOPREAL9: 18;

          assume

           A18: WB is empty;

          

          then (W /\ ( cl_Ball (( 0. TR),1))) = ((W /\ ( cl_Ball (( 0. TR),1))) \ WB)

          .= (((W /\ ( cl_Ball (( 0. TR),1))) \ W) \/ ((W /\ ( cl_Ball (( 0. TR),1))) \ ( Ball (( 0. TR),1)))) by XBOOLE_1: 54

          .= ( {} \/ ((W /\ ( cl_Ball (( 0. TR),1))) \ ( Ball (( 0. TR),1)))) by XBOOLE_1: 17, XBOOLE_1: 37

          .= (W /\ (( cl_Ball (( 0. TR),1)) \ ( Ball (( 0. TR),1)))) by XBOOLE_1: 49

          .= (W /\ ( Sphere (( 0. TR),1))) by A16, A17, XBOOLE_1: 88;

          then hp in ( Sphere (( 0. TR),1)) by A15, A13, XBOOLE_0:def 4;

          then

           A19: |.hp.| = 1 by TOPREAL9: 12;

          ( Int W) = W by TOPS_1: 23;

          then

          consider s be Real such that

           A20: s > 0 and

           A21: ( Ball (HP,s)) c= W by A14, GOBOARD6: 5;

          set s2 = (s / 2), m = ( min ((s / 2),(1 / 2)));

          

           A22: m <= s2 by XXREAL_0: 17;

          s2 < s by A20, XREAL_1: 216;

          then

           A23: m < s by A22, XXREAL_0: 2;

          

           A24: ( Ball (HP,s)) = ( Ball (hp,s)) by TOPREAL9: 13;

          

           A25: m > 0 by A20, XXREAL_0: 21;

          then

           A26: (1 - m) < (1 - 0 ) by XREAL_1: 6;

          

           A27: |.( - m).| = ( - ( - m)) by A25, ABSVALUE:def 1;

          

           A28: (((1 - m) * hp) - ( 0. TR)) = ((1 - m) * hp) by RLVECT_1: 13;

          (((1 - m) * hp) - hp) = (((1 - m) * hp) - (1 * hp)) by RLVECT_1:def 8

          .= (((1 - m) - 1) * hp) by RLVECT_1: 35

          .= (( - m) * hp);

          then |.(((1 - m) * hp) - hp).| = ( |.( - m).| * 1) by A19, EUCLID: 11;

          then

           A29: ((1 - m) * hp) in ( Ball (hp,s)) by A27, A23;

          (1 - m) >= (1 - (1 / 2)) by XXREAL_0: 17, XREAL_1: 10;

          then |.(1 - m).| = (1 - m) by ABSVALUE:def 1;

          then |.((1 - m) * hp).| = ((1 - m) * 1) by A19, EUCLID: 11;

          then ((1 - m) * hp) in ( Ball (( 0. TR),1)) by A28, A26;

          hence thesis by A29, A21, A24, A18, XBOOLE_0:def 4;

        end;

        then

        consider wb be set such that

         A30: wb in WB;

        reconsider wb as Point of TR by A30;

        reconsider wbE = wb as Point of ( Euclid n) by EUCLID: 67;

        ( Int WB) = WB by TOPS_1: 23;

        then

        consider s be Real such that

         A31: s > 0 and

         A32: ( Ball (wbE,s)) c= WB by A30, GOBOARD6: 5;

        

         A33: ( Ball (wb,s)) = ( Ball (wbE,s)) by TOPREAL9: 13;

        WB c= ( Ball (( 0. TR),1)) by XBOOLE_1: 17;

        then

         A34: ( Ball (wb,s)) c= ( Ball (( 0. TR),1)) by A32, A33;

        then

        reconsider BB = ( Ball (wb,s)) as Subset of ( Tdisk (( 0. TR),1)) by A12, XBOOLE_1: 1, A10;

        

         A35: (( Tdisk (( 0. TR),1)) | BB) = (TR | ( Ball (wb,s))) by A34, A12, XBOOLE_1: 1, PRE_TOPC: 7;

        reconsider hBB = (h " BB) as Subset of M by A6, XBOOLE_1: 1;

        BB is open by TSEP_1: 9;

        then

         A36: (h " BB) is open by A7, TOPGRP_1: 26;

        WB c= (h .: IU) by A10, A9, TOPREAL9: 16, XBOOLE_1: 26;

        then BB c= (h .: IU) by A32, A33;

        then

         A37: (h " BB) c= (h " (h .: IU)) by RELAT_1: 143;

        (h " (h .: IU)) c= IU by FUNCT_1: 82, A7;

        then (h " BB) c= IU by A37;

        then hBB is open by A36, TSEP_1: 9;

        then

         A38: ( Int hBB) = hBB by TOPS_1: 23;

        

         A39: ( rng h) = ( [#] ( Tdisk (( 0. TR),1))) by A7, TOPS_2:def 5;

        then

         A40: (h .: (h " BB)) = BB by FUNCT_1: 77;

        hBB is non empty by A31, RELAT_1: 139, A39;

        then

        consider t be set such that

         A41: t in hBB;

        reconsider t as Point of M by A41;

        reconsider hBB as a_neighborhood of t by A38, CONNSP_2:def 1, A41;

        

         A43: (MU | (h " BB)) = (M | hBB) by A6, PRE_TOPC: 7;

        then

        reconsider HH = (h | (h " BB)) as Function of (M | hBB), (TR | ( Ball (wb,s))) by A40, A35, JORDAN24: 12;

        HH is being_homeomorphism by A7, A40, A35, A43, METRIZTS: 2;

        then

         A44: ((M | hBB),(TR | ( Ball (wb,s)))) are_homeomorphic by T_0TOPSP:def 1;

        (( Tball (wb,s)),( Tball (( 0. TR),1))) are_homeomorphic by Th3, A31;

        then ((M | hBB),( Tball (( 0. TR),1))) are_homeomorphic by A44, A31, BORSUK_3: 3;

        hence thesis by A1, TOPS_1: 25, Def4;

      end;

    end

    definition

      let M be non empty TopSpace;

      :: MFOLD_0:def5

      func Fr M -> Subset of M equals (( Int M) ` );

      coherence ;

    end

    ::$Notion-Name

    theorem :: MFOLD_0:5

    

     Th5: for M be locally_euclidean non empty TopSpace holds for p be Point of M holds p in ( Fr M) iff ex U be a_neighborhood of p, n be Nat, h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL n)),1)) st h is being_homeomorphism & (h . p) in ( Sphere (( 0. ( TOP-REAL n)),1))

    proof

      let M be locally_euclidean non empty TopSpace;

      let p be Point of M;

      thus p in ( Fr M) implies ex U be a_neighborhood of p, n be Nat, h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL n)),1)) st h is being_homeomorphism & (h . p) in ( Sphere (( 0. ( TOP-REAL n)),1))

      proof

        assume

         A1: p in ( Fr M);

        consider U be a_neighborhood of p, n such that

         A2: ((M | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Def2;

        set TR = ( TOP-REAL n);

        consider h be Function of (M | U), ( Tdisk (( 0. TR),1)) such that

         A3: h is being_homeomorphism by A2, T_0TOPSP:def 1;

        assume for U be a_neighborhood of p, n be Nat, h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL n)),1)) st h is being_homeomorphism holds not (h . p) in ( Sphere (( 0. ( TOP-REAL n)),1));

        then

         A4: not (h . p) in ( Sphere (( 0. TR),1)) by A3;

        

         A5: ( Ball (( 0. TR),1)) in the topology of TR by PRE_TOPC:def 2;

        

         A6: p in ( Int U) by CONNSP_2:def 1;

        

         A7: ( Int U) in the topology of M by PRE_TOPC:def 2;

        

         A8: ( [#] (M | U)) = U by PRE_TOPC:def 5;

        then

        reconsider IU = ( Int U) as Subset of (M | U) by TOPS_1: 16;

        (IU /\ U) = IU by TOPS_1: 16, XBOOLE_1: 28;

        then IU in the topology of (M | U) by A7, A8, PRE_TOPC:def 4;

        then

        reconsider IU as non empty open Subset of (M | U) by CONNSP_2:def 1, PRE_TOPC:def 2;

        

         A9: ( [#] (TR | ( cl_Ball (( 0. TR),1)))) = ( cl_Ball (( 0. TR),1)) by PRE_TOPC:def 5;

        then

        reconsider hIU = (h .: IU) as Subset of TR by XBOOLE_1: 1;

        

         A10: (h .: IU) is open by A3, TOPGRP_1: 25;

        

         A11: ( dom h) = ( [#] (M | U)) by A3, TOPS_2:def 5;

        then

         A12: (h " (h .: IU)) = IU by FUNCT_1: 94, A3;

        

         A13: ( cl_Ball (( 0. TR),1)) = (( Ball (( 0. TR),1)) \/ ( Sphere (( 0. TR),1))) by TOPREAL9: 18;

        then

        reconsider B = ( Ball (( 0. TR),1)) as Subset of (TR | ( cl_Ball (( 0. TR),1))) by A9, XBOOLE_1: 7;

        (( Ball (( 0. TR),1)) /\ ( cl_Ball (( 0. TR),1))) = ( Ball (( 0. TR),1)) by A13, XBOOLE_1: 7, XBOOLE_1: 28;

        then B in the topology of (TR | ( cl_Ball (( 0. TR),1))) by A5, A9, PRE_TOPC:def 4;

        then

        reconsider B as non empty open Subset of (TR | ( cl_Ball (( 0. TR),1))) by PRE_TOPC:def 2;

        reconsider BhIU = (B /\ (h .: IU)) as Subset of TR by XBOOLE_1: 1, A9;

        BhIU c= ( Ball (( 0. TR),1)) by XBOOLE_1: 17;

        then

         A14: BhIU is open by A10, TSEP_1: 9;

        

         A15: ( Int U) c= U by TOPS_1: 16;

        then (h . p) in ( rng h) by A6, A8, A11, FUNCT_1:def 3;

        then

         A16: (h . p) in ( Ball (( 0. TR),1)) by A4, A9, A13, XBOOLE_0:def 3;

        then

        reconsider hp = (h . p) as Point of TR;

         the TopStruct of TR = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

        then

        reconsider HP = hp as Point of ( Euclid n) by TOPMETR: 12;

        (h . p) in (h .: IU) by A11, A6, FUNCT_1:def 6;

        then (h . p) in BhIU by A16, XBOOLE_0:def 4;

        then hp in ( Int BhIU) by A14, TOPS_1: 23;

        then

        consider s be Real such that

         A17: s > 0 and

         A18: ( Ball (HP,s)) c= BhIU by GOBOARD6: 5;

        set W = ( Ball (hp,s));

        reconsider hW = (h " W) as Subset of M by A8, XBOOLE_1: 1;

        

         A19: W c= (B /\ (h .: IU)) by A18, TOPREAL9: 13;

        then

        reconsider w = W as Subset of (TR | ( cl_Ball (( 0. TR),1))) by XBOOLE_1: 1;

        

         A20: w in the topology of TR by PRE_TOPC:def 2;

        hp is Element of ( REAL n) by EUCLID: 22;

        then |.(hp - hp).| = 0 ;

        then hp in ( Ball (hp,s)) by A17;

        then

         A21: p in hW by A8, A11, A15, A6, FUNCT_1:def 7;

        ( rng h) = ( [#] (TR | ( cl_Ball (( 0. TR),1)))) by A3, TOPS_2:def 5;

        then (h .: (h " W)) = W by A19, XBOOLE_1: 1, FUNCT_1: 77;

        then

         A22: (( Tdisk (( 0. TR),1)) | (h .: (h " W))) = (TR | W) by A9, PRE_TOPC: 7;

        (w /\ ( cl_Ball (( 0. TR),1))) = w by A9, XBOOLE_1: 28;

        then

         A23: w in the topology of (TR | ( cl_Ball (( 0. TR),1))) by A9, A20, PRE_TOPC:def 4;

        (B /\ (h .: IU)) c= (h .: IU) by XBOOLE_1: 17;

        then W c= (h .: IU) by A19;

        then

         A24: hW c= IU by A12, RELAT_1: 143;

        reconsider w as open Subset of (TR | ( cl_Ball (( 0. TR),1))) by A23, PRE_TOPC:def 2;

        reconsider hh = (h | (h " w)) as Function of ((M | U) | (h " w)), (( Tdisk (( 0. TR),1)) | (h .: (h " w))) by JORDAN24: 12;

        

         A25: ((M | U) | (h " W)) = (M | hW) by A8, PRE_TOPC: 7;

        then

        reconsider HH = hh as Function of (M | hW), (TR | W) by A22;

        (h " w) is open by A3, TOPGRP_1: 26;

        then hW is open by A24, TSEP_1: 9;

        then p in ( Int hW) by A21, TOPS_1: 23;

        then

        reconsider HW = hW as a_neighborhood of p by CONNSP_2:def 1;

        HH is being_homeomorphism by A3, METRIZTS: 2, A22, A25;

        then

         A27: ((M | HW),(TR | W)) are_homeomorphic by T_0TOPSP:def 1;

        (( Tball (hp,s)),( Tball (( 0. TR),1))) are_homeomorphic by A17, Th3;

        then ((M | HW),( Tball (( 0. TR),1))) are_homeomorphic by A27, A17, BORSUK_3: 3;

        then p in ( Int M) by Def4;

        then not p in (( [#] M) \ ( Int M)) by XBOOLE_0:def 5;

        hence contradiction by SUBSET_1:def 4, A1;

      end;

      given U be a_neighborhood of p, n be Nat, h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL n)),1)) such that

       A28: h is being_homeomorphism and

       A29: (h . p) in ( Sphere (( 0. ( TOP-REAL n)),1));

      set TR = ( TOP-REAL n);

      

       A30: p in ( Int U) by CONNSP_2:def 1;

      assume not p in ( Fr M);

      then not p in (( [#] M) \ ( Int M)) by SUBSET_1:def 4;

      then p in ( Int M) by XBOOLE_0:def 5;

      then

      consider W be a_neighborhood of p, m such that

       A31: ((M | W),( Tball (( 0. ( TOP-REAL m)),1))) are_homeomorphic by Def4;

      

       A33: p in ( Int W) by CONNSP_2:def 1;

      ((M | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A28, T_0TOPSP:def 1;

      then m = n by A30, A33, XBOOLE_0: 3, BROUWER3: 15, A31;

      then

      consider g be Function of (M | W), (TR | ( Ball (( 0. TR),1))) such that

       A34: g is being_homeomorphism by A31, T_0TOPSP:def 1;

      

       A35: ( Int U) c= U by TOPS_1: 16;

      set I = (( Int U) /\ ( Int W));

      

       A36: ( [#] (M | U)) = U by PRE_TOPC:def 5;

      I c= ( Int U) by XBOOLE_1: 17;

      then

      reconsider IU = I as non empty open Subset of (M | U) by XBOOLE_1: 1, A35, A36, A30, A33, XBOOLE_0:def 4, TSEP_1: 9;

      

       A37: ( dom h) = ( [#] (M | U)) by A28, TOPS_2:def 5;

      then

       A38: (h " (h .: IU)) = IU by A28, FUNCT_1: 94;

      p in I by A30, A33, XBOOLE_0:def 4;

      then

       A39: (h . p) in (h .: IU) by A37, FUNCT_1:def 6;

      (h .: IU) is open by A28, TOPGRP_1: 25;

      then (h .: IU) in the topology of (TR | ( cl_Ball (( 0. TR),1))) by PRE_TOPC:def 2;

      then

      consider Q be Subset of TR such that

       A40: Q in the topology of TR and

       A41: (h .: IU) = (Q /\ ( [#] (TR | ( cl_Ball (( 0. TR),1))))) by PRE_TOPC:def 4;

      reconsider Q as non empty Subset of TR by A41;

      

       A42: ( Int Q) = Q by A40, PRE_TOPC:def 2, TOPS_1: 23;

      

       A43: I c= ( Int W) by XBOOLE_1: 17;

      

       A44: ( [#] (TR | ( cl_Ball (( 0. TR),1)))) = ( cl_Ball (( 0. TR),1)) by PRE_TOPC:def 5;

      then (h . p) in ( cl_Ball (( 0. TR),1)) by A39;

      then

      reconsider hp = (h . p) as Point of TR;

       the TopStruct of TR = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      then

      reconsider HP = hp as Point of ( Euclid n) by TOPMETR: 12;

      hp in Q by A39, A41, XBOOLE_0:def 4;

      then

      consider s be Real such that

       A45: s > 0 and

       A46: ( Ball (HP,s)) c= Q by A42, GOBOARD6: 5;

      set s2 = (s / 2);

      hp is Element of ( REAL n) by EUCLID: 22;

      then |.(hp - hp).| = 0 ;

      then

       A47: hp in ( Ball (hp,s2)) by A45;

      set clb = (( cl_Ball (hp,s2)) /\ ( cl_Ball (( 0. TR),1)));

      

       A48: ( Ball (hp,s2)) c= ( cl_Ball (hp,s2)) by TOPREAL9: 16;

      clb = (( cl_Ball (hp,s2)) /\ ( [#] (TR | ( cl_Ball (( 0. TR),1))))) by PRE_TOPC:def 5;

      then

      reconsider CLB = clb as non empty Subset of (TR | ( cl_Ball (( 0. TR),1))) by A48, A47, A39, XBOOLE_0:def 4;

      

       A49: ( rng h) = ( [#] (TR | ( cl_Ball (( 0. TR),1)))) by A28, TOPS_2:def 5;

      then

      reconsider hCLB = (h " CLB) as non empty Subset of (M | U) by RELAT_1: 139;

      

       A50: ( Ball (HP,s)) = ( Ball (hp,s)) by TOPREAL9: 13;

      hp in CLB by A48, A47, A39, A44, XBOOLE_0:def 4;

      then

       A51: p in hCLB by A37, A36, A35, A30, FUNCT_1:def 7;

      n in NAT by ORDINAL1:def 12;

      then

       A52: ( cl_Ball (hp,s2)) c= ( Ball (hp,s)) by XREAL_1: 216, A45, JORDAN: 21;

      then ( cl_Ball (hp,s2)) c= Q by A46, A50;

      then CLB c= (h .: IU) by A44, XBOOLE_1: 26, A41;

      then

       A53: hCLB c= IU by RELAT_1: 143, A38;

      reconsider BB = (( Ball (hp,s2)) /\ ( [#] (TR | ( cl_Ball (( 0. TR),1))))) as Subset of (TR | ( cl_Ball (( 0. TR),1)));

      reconsider hBB = (h " BB) as Subset of M by A36, XBOOLE_1: 1;

      ( Ball (hp,s2)) c= Q by A46, A50, A48, A52;

      then BB c= (h .: IU) by XBOOLE_1: 26, A41;

      then

       A54: (h " BB) c= IU by RELAT_1: 143, A38;

      reconsider HCLB = hCLB as non empty Subset of M by A36, XBOOLE_1: 1;

      

       A55: (h .: hCLB) = CLB by A49, FUNCT_1: 77;

      

       A56: ((TR | ( cl_Ball (( 0. TR),1))) | CLB) = (TR | clb) by A44, PRE_TOPC: 7;

      

       A57: ((M | U) | hCLB) = (M | HCLB) by A36, PRE_TOPC: 7;

      then

      reconsider h1 = (h | hCLB) as Function of (M | HCLB), (TR | clb) by A56, A55, JORDAN24: 12;

      

       A58: ( Int W) c= W by TOPS_1: 16;

      

       A59: ( [#] (M | W)) = W by PRE_TOPC:def 5;

      then

      reconsider IW = I as non empty open Subset of (M | W) by A30, A33, XBOOLE_0:def 4, XBOOLE_1: 1, A58, A43, TSEP_1: 9;

      

       A60: IU c= W by A58, A43;

      then

      reconsider hCLW = hCLB as non empty Subset of (M | W) by A53, XBOOLE_1: 1, A59;

      

       A61: ((M | W) | hCLW) = (M | HCLB) by A53, A60, XBOOLE_1: 1, PRE_TOPC: 7;

      set ghCLW = (g .: hCLW);

      

       A62: ( [#] (TR | ( Ball (( 0. TR),1)))) = ( Ball (( 0. TR),1)) by PRE_TOPC:def 5;

      then

      reconsider GhCLW = ghCLW as non empty Subset of TR by XBOOLE_1: 1;

      

       A63: ((TR | ( Ball (( 0. TR),1))) | ghCLW) = (TR | GhCLW) by A62, PRE_TOPC: 7;

      then

      reconsider g1 = (g | hCLB) as Function of (M | HCLB), (TR | GhCLW) by A61, JORDAN24: 12;

      

       A64: g1 is being_homeomorphism by A34, METRIZTS: 2, A63, A61;

      then

       A65: (g1 " ) is being_homeomorphism by TOPS_2: 56;

      

       A66: ( dom g) = ( [#] (M | W)) by A34, TOPS_2:def 5;

      then (g . p) in GhCLW by A51, FUNCT_1:def 6;

      then

      reconsider gp = (g . p) as Point of TR;

      I c= W by A58, A43;

      then

      reconsider hBW = hBB as Subset of (M | W) by A54, XBOOLE_1: 1, A59;

      reconsider ghBW = (g .: hBW) as Subset of TR by A62, XBOOLE_1: 1;

      hp in BB by A47, A39, XBOOLE_0:def 4;

      then p in (h " BB) by A37, A36, A35, A30, FUNCT_1:def 7;

      then

       A67: gp in ghBW by A66, FUNCT_1:def 6;

      set hg = (h1 * (g1 " ));

      h1 is being_homeomorphism by A28, A56, METRIZTS: 2, A57, A55;

      then

       A68: hg is being_homeomorphism by A65, TOPS_2: 57;

      then

       A69: ( dom hg) = ( [#] (TR | GhCLW)) by TOPS_2:def 5;

      BB c= clb by TOPREAL9: 16, XBOOLE_1: 26, A44;

      then

       A70: hBB c= hCLB by RELAT_1: 143;

      then ghBW c= GhCLW by RELAT_1: 123;

      then gp in GhCLW by A67;

      then

       A71: gp in ( dom hg) by A69, PRE_TOPC:def 5;

      ( Ball (hp,s2)) in the topology of TR by PRE_TOPC:def 2;

      then BB in the topology of (TR | ( cl_Ball (( 0. TR),1))) by PRE_TOPC:def 4;

      then BB is non empty open by A47, A39, XBOOLE_0:def 4, PRE_TOPC:def 2;

      then (h " BB) is open by A28, TOPGRP_1: 26;

      then hBB is open by A54, TSEP_1: 9;

      then hBW is open by TSEP_1: 9;

      then (g .: hBW) is open by A34, TOPGRP_1: 25;

      then ghBW is open by A62, TSEP_1: 9;

      then gp in ( Int GhCLW) by A67, TOPS_1: 22, A70, RELAT_1: 123;

      then

       A72: (hg . gp) in ( Int clb) by BROUWER3: 11, A68;

      ( Int clb) = (( Int ( cl_Ball (hp,s2))) /\ ( Int ( cl_Ball (( 0. TR),1)))) by TOPS_1: 17;

      then

       A73: (hg . gp) in ( Int ( cl_Ball (( 0. TR),1))) by A72, XBOOLE_0:def 4;

      reconsider G1 = g1 as Function;

      ( Fr ( cl_Ball (( 0. TR),1))) = ( Sphere (( 0. TR),1)) by BROUWER2: 5;

      then

       A74: ( Int ( cl_Ball (( 0. TR),1))) = (( cl_Ball (( 0. TR),1)) \ ( Sphere (( 0. TR),1))) by TOPS_1: 40;

      

       A75: (G1 " ) = (g1 " ) by A64, TOPS_2:def 4;

      ( dom g1) = ( [#] (M | HCLB)) by A64, TOPS_2:def 5;

      then p in ( dom g1) by PRE_TOPC:def 5, A51;

      then

       A76: ((g1 " ) . (g1 . p)) = p by A64, A75, FUNCT_1: 34;

      

       A77: (g . p) = (g1 . p) by A51, FUNCT_1: 49;

      then

       A78: p in ( dom h1) by A71, FUNCT_1: 11, A76;

      (hg . gp) = (h1 . p) by A71, FUNCT_1: 12, A76, A77;

      then (hg . gp) = (h . p) by A78, FUNCT_1: 47;

      hence contradiction by A29, A73, A74, XBOOLE_0:def 5;

    end;

    begin

    definition

      let M be non empty TopSpace;

      :: MFOLD_0:def6

      attr M is without_boundary means

      : Def6: ( Int M) = the carrier of M;

    end

    notation

      let M be non empty TopSpace;

      antonym M is with_boundary for M is without_boundary;

    end

    

     Lm2: (M is locally_euclidean without_boundary) iff for p be Point of M holds ex U be a_neighborhood of p, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic

    proof

      hereby

        assume that

         A1: M is locally_euclidean without_boundary;

        let p be Point of M;

        consider U be a_neighborhood of p, n such that

         A2: ((M | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A1;

        set MU = (M | U);

        set TR = ( TOP-REAL n);

        consider h be Function of MU, ( Tdisk (( 0. TR),1)) such that

         A3: h is being_homeomorphism by A2, T_0TOPSP:def 1;

        

         A4: ( cl_Ball (( 0. TR),1)) = (( Ball (( 0. TR),1)) \/ ( Sphere (( 0. TR),1))) by TOPREAL9: 18;

        

         A5: ( [#] ( Tdisk (( 0. TR),1))) = ( cl_Ball (( 0. TR),1)) by PRE_TOPC:def 5;

        then

        reconsider B = ( Ball (( 0. TR),1)) as Subset of ( Tdisk (( 0. TR),1)) by TOPREAL9: 16;

        

         A6: ( [#] MU) = U by PRE_TOPC:def 5;

        then

        reconsider IU = ( Int U) as Subset of (M | U) by TOPS_1: 16;

        

         A7: p in ( Int U) by CONNSP_2:def 1;

        reconsider B as open Subset of ( Tdisk (( 0. TR),1)) by TSEP_1: 9;

        set HIB = (B /\ (h .: ( Int U)));

        reconsider hib = HIB as Subset of TR by A5, XBOOLE_1: 1;

        

         A8: HIB c= ( Ball (( 0. TR),1)) by XBOOLE_1: 17;

        IU is open by TSEP_1: 9;

        then (h .: ( Int U)) is open by A3, TOPGRP_1: 25;

        then

         A9: hib is open by TSEP_1: 9, A8;

        reconsider MM = M as locally_euclidean non empty TopSpace by A1;

        

         A10: ( Int U) c= U by TOPS_1: 16;

        

         A11: ( dom h) = ( [#] MU) by A3, TOPS_2:def 5;

        then

         A12: (h . p) in ( rng h) by A7, A10, A6, FUNCT_1:def 3;

        

         A13: (h . p) in ( Ball (( 0. TR),1))

        proof

          assume not (h . p) in ( Ball (( 0. TR),1));

          then

           A14: (h . p) in ( Sphere (( 0. TR),1)) by A5, A12, A4, XBOOLE_0:def 3;

          ( Fr MM) = (the carrier of MM \ ( Int MM)) by SUBSET_1:def 4

          .= {} by XBOOLE_1: 37, A1;

          hence contradiction by A14, A3, Th5;

        end;

        then

        reconsider hP = (h . p) as Point of TR;

        (h . p) in (h .: ( Int U)) by A7, A10, A6, A11, FUNCT_1:def 6;

        then (h . p) in hib by A13, XBOOLE_0:def 4;

        then

        consider r be positive Real such that

         A15: ( Ball (hP,r)) c= hib by A9, TOPS_4: 2;

         |.(hP - hP).| = 0 by TOPRNS_1: 28;

        then

         A16: hP in ( Ball (hP,r));

        reconsider bb = ( Ball (hP,r)) as non empty Subset of ( Tdisk (( 0. TR),1)) by A15, XBOOLE_1: 1;

        reconsider hb = (h " bb) as Subset of M by A6, XBOOLE_1: 1;

        bb is open by TSEP_1: 9;

        then

         A17: (h " bb) is open by A3, TOPGRP_1: 26;

        

         A18: (h " HIB) c= (h " (h .: ( Int U))) by XBOOLE_1: 17, RELAT_1: 143;

        

         A19: (h " (h .: ( Int U))) c= ( Int U) by A3, FUNCT_1: 82;

        

         A20: (M | hb) = ((M | U) | (h " bb)) by A6, PRE_TOPC: 7;

        hb c= (h " HIB) by A15, RELAT_1: 143;

        then hb c= ( Int U) by A18, A19;

        then

         A21: hb is open by A6, TSEP_1: 9, A17, A10;

        p in hb by A16, A7, A10, A6, A11, FUNCT_1:def 7;

        then

         A22: p in ( Int hb) by A21, TOPS_1: 23;

        ( rng h) = ( [#] ( Tdisk (( 0. TR),1))) by A3, TOPS_2:def 5;

        then

         A23: (h .: (h " bb)) = bb by FUNCT_1: 77;

        

         A25: (( Tdisk (( 0. TR),1)) | bb) = (TR | ( Ball (hP,r))) by A5, PRE_TOPC: 7;

        then

        reconsider hh = (h | (h " bb)) as Function of (M | hb), ( Tball (hP,r)) by A20, JORDAN24: 12, A23;

        reconsider hb as a_neighborhood of p by A22, CONNSP_2:def 1;

        hh is being_homeomorphism by A3, A20, A23, A25, METRIZTS: 2;

        then

         A26: ((M | hb),( Tball (hP,r))) are_homeomorphic by T_0TOPSP:def 1;

        take hb;

        take n;

        (( Tball (hP,r)),( Tball (( 0. TR),1))) are_homeomorphic by Th3;

        hence ((M | hb),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A26, BORSUK_3: 3;

      end;

      assume

       A27: for p be Point of M holds ex U be a_neighborhood of p, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

      thus M is locally_euclidean

      proof

        let p be Point of M;

        consider U be a_neighborhood of p, n such that

         A28: ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A27;

        set En = ( Euclid n);

        set TR = ( TOP-REAL n);

        

         A29: ( Int U) c= U by TOPS_1: 16;

        ( [#] ( Tdisk (( 0. TR),1))) = ( cl_Ball (( 0. TR),1)) by PRE_TOPC:def 5;

        then

        reconsider B = ( Ball (( 0. TR),1)) as Subset of ( Tdisk (( 0. TR),1)) by TOPREAL9: 16;

        set MU = (M | U);

        consider h be Function of MU, ( Tball (( 0. ( TOP-REAL n)),1)) such that

         A30: h is being_homeomorphism by A28, T_0TOPSP:def 1;

        

         A31: n in NAT by ORDINAL1:def 12;

        

         A33: ( [#] ( Tball (( 0. TR),1))) = ( Ball (( 0. TR),1)) by PRE_TOPC:def 5;

        then

        reconsider clB = ( cl_Ball (( 0. TR),(1 / 2))) as non empty Subset of ( Tball (( 0. TR),1)) by JORDAN: 21, A31;

        

         A34: ( [#] MU) = U by PRE_TOPC:def 5;

        then

        reconsider IU = ( Int U) as Subset of (M | U) by TOPS_1: 16;

        reconsider hIU = (h .: IU) as Subset of TR by A33, XBOOLE_1: 1;

        

         A35: ( dom h) = ( [#] MU) by A30, TOPS_2:def 5;

        then

         A36: IU = (h " hIU) by A30, FUNCT_1: 82, FUNCT_1: 76;

        

         A37: the TopStruct of TR = ( TopSpaceMetr En) by EUCLID:def 8;

        then

        reconsider hIUE = hIU as Subset of ( TopSpaceMetr En);

        

         A38: p in ( Int U) by CONNSP_2:def 1;

        then

         A39: (h . p) in hIU by A35, FUNCT_1:def 6;

        then

        reconsider hp = (h . p) as Point of En by EUCLID: 67;

        reconsider Hp = (h . p) as Point of TR by A39;

        IU is open by TSEP_1: 9;

        then (h .: IU) is open by A30, TOPGRP_1: 25;

        then hIU is open by A33, TSEP_1: 9;

        then hIU in the topology of TR by PRE_TOPC:def 2;

        then

        consider r be Real such that

         A40: r > 0 and

         A41: ( Ball (hp,r)) c= hIUE by A39, A37, PRE_TOPC:def 2, TOPMETR: 15;

        set r2 = (r / 2);

        

         A42: ( Ball (Hp,r)) = ( Ball (hp,r)) by TOPREAL9: 13;

        ( cl_Ball (Hp,r2)) c= ( Ball (Hp,r)) by A31, XREAL_1: 216, A40, JORDAN: 21;

        then

         A43: ( cl_Ball (Hp,r2)) c= hIU by A41, A42;

        then

        reconsider CL = ( cl_Ball (Hp,r2)) as Subset of ( Tball (( 0. TR),1)) by XBOOLE_1: 1;

        

         A44: ( cl_Ball (Hp,r2)) c= ( [#] ( Tball (( 0. TR),1))) by A43, XBOOLE_1: 1;

        then ( cl_Ball (Hp,r2)) c= ( rng h) by A30, TOPS_2:def 5;

        then

         A45: (h .: (h " CL)) = CL by FUNCT_1: 77;

        set r22 = (r2 / 2);

        r22 < r2 by A40, XREAL_1: 216;

        then

         A46: ( Ball (Hp,r22)) c= ( Ball (Hp,r2)) by A31, JORDAN: 18;

        reconsider hCL = (h " CL) as Subset of M by A34, XBOOLE_1: 1;

        

         A47: ((M | U) | (h " CL)) = (M | hCL) by A34, PRE_TOPC: 7;

        

         A48: ( Ball (Hp,r2)) c= ( cl_Ball (Hp,r2)) by TOPREAL9: 16;

        then

         A49: ( Ball (Hp,r22)) c= ( cl_Ball (Hp,r2)) by A46;

        then

        reconsider BI = ( Ball (Hp,r22)) as Subset of ( Tball (( 0. TR),1)) by A44, XBOOLE_1: 1;

        BI c= hIU by A43, A48, A46;

        then

         A50: (h " BI) c= (h " hIU) by RELAT_1: 143;

        reconsider hBI = (h " BI) as Subset of M by A34, XBOOLE_1: 1;

        BI is open by TSEP_1: 9;

        then (h " BI) is open by A30, TOPGRP_1: 26;

        then

         A51: hBI is open by A36, A50, TSEP_1: 9;

         |.(Hp - Hp).| = 0 by TOPRNS_1: 28;

        then (h . p) in BI by A40;

        then p in (h " BI) by A38, A29, A34, A35, FUNCT_1:def 7;

        then p in ( Int hCL) by A49, RELAT_1: 143, TOPS_1: 22, A51;

        then

        reconsider hCL as a_neighborhood of p by CONNSP_2:def 1;

        

         A52: (( Tball (( 0. TR),1)) | CL) = ( Tdisk (Hp,r2)) by A33, PRE_TOPC: 7;

        then

        reconsider hh = (h | (h " CL)) as Function of (M | hCL), ( Tdisk (Hp,r2)) by A45, JORDAN24: 12, A47;

        hh is being_homeomorphism by A30, A52, METRIZTS: 2, A45, A47;

        then

         A53: ((M | hCL),( Tdisk (Hp,r2))) are_homeomorphic by T_0TOPSP:def 1;

        (( Tdisk (Hp,r2)),( Tdisk (( 0. TR),1))) are_homeomorphic by Lm1, A40;

        hence thesis by A53, BORSUK_3: 3, A40;

      end;

      thus ( Int M) c= the carrier of M;

      let x be object;

      assume x in the carrier of M;

      then

      reconsider p = x as Point of M;

      ex U be a_neighborhood of p, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A27;

      hence thesis by Def4;

    end;

    

     Lm3: ( Tball (( 0. ( TOP-REAL n)),1)) is n -locally_euclidean without_boundary

    proof

      set TR = ( TOP-REAL n);

      set M = ( Tball (( 0. TR),1));

      

       A1: for p be Point of M holds ex U be a_neighborhood of p st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic

      proof

        let p be Point of M;

        ( Int ( [#] M)) = ( [#] M) by TOPS_1: 15;

        then

        reconsider CM = ( [#] M) as non empty a_neighborhood of p by CONNSP_2:def 1;

        take CM;

        thus thesis by TSEP_1: 93;

      end;

      

       A2: for p be Point of M holds ex U be a_neighborhood of p, m st ((M | U),( Tball (( 0. ( TOP-REAL m)),1))) are_homeomorphic

      proof

        let p be Point of M;

        ex U be a_neighborhood of p st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A1;

        hence ex U be a_neighborhood of p, m st ((M | U),( Tball (( 0. ( TOP-REAL m)),1))) are_homeomorphic ;

      end;

      then

      reconsider MM = M as locally_euclidean non empty TopSpace by Lm2;

      MM is n -locally_euclidean

      proof

        let p be Point of MM;

        consider U be a_neighborhood of p such that

         A3: ((MM | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A1;

        

         A5: p in ( Int U) by CONNSP_2:def 1;

        consider W be a_neighborhood of p, m such that

         A6: ((MM | W),( Tdisk (( 0. ( TOP-REAL m)),1))) are_homeomorphic by Def2;

        p in ( Int W) by CONNSP_2:def 1;

        then m = n by A5, XBOOLE_0: 3, A3, A6, BROUWER3: 15;

        hence thesis by A6;

      end;

      hence thesis by A2, Lm2;

    end;

    registration

      let n;

      cluster ( Tball (( 0. ( TOP-REAL n)),1)) -> without_boundaryn -locally_euclidean;

      coherence by Lm3;

    end

    registration

      let n be non zero Nat;

      cluster ( Tdisk (( 0. ( TOP-REAL n)),1)) -> with_boundary;

      coherence

      proof

        set TR = ( TOP-REAL n);

        set M = ( Tdisk (( 0. TR),1));

        reconsider CM = ( [#] M) as non empty Subset of M;

        consider p be object such that

         A1: p in ( Sphere (( 0. TR),1)) by XBOOLE_0:def 1;

        reconsider p as Point of TR by A1;

        

         A2: ( [#] M) = ( cl_Ball (( 0. TR),1)) by PRE_TOPC:def 5;

        ( Sphere (( 0. TR),1)) c= ( cl_Ball (( 0. TR),1)) by TOPREAL9: 17;

        then

        reconsider pp = p as Point of M by A2, A1;

        

         A3: ( Fr ( cl_Ball (( 0. TR),1))) = ( Sphere (( 0. TR),1)) by BROUWER2: 5;

        ( [#] (M | CM)) = CM by PRE_TOPC:def 5;

        then

        reconsider cm = CM as non empty Subset of (M | CM);

        ( Int ( [#] M)) = ( [#] M) by TOPS_1: 15;

        then

        reconsider CM as non empty a_neighborhood of pp by CONNSP_2:def 1;

        

         A4: (M | CM) = M by TSEP_1: 3;

        ( Ball (( 0. TR),1)) c= ( Int ( cl_Ball (( 0. TR),1))) by TOPREAL9: 16, TOPS_1: 24;

        then ( cl_Ball (( 0. TR),1)) is non boundary compact;

        then

        consider h be Function of (M | CM), M such that

         A5: h is being_homeomorphism and

         A6: (h .: ( Fr ( cl_Ball (( 0. TR),1)))) = ( Fr ( cl_Ball (( 0. TR),1))) by BROUWER2: 7, A4;

        ( dom h) = ( [#] M) by A5, A4, TOPS_2:def 5;

        then

         A7: (h . pp) in (h .: ( Sphere (( 0. TR),1))) by A1, FUNCT_1:def 6;

        M is with_boundary

        proof

          assume

           A8: M is without_boundary;

          ( Fr M) = (the carrier of M \ the carrier of M) by A8, SUBSET_1:def 4

          .= {} by XBOOLE_1: 37;

          hence thesis by A3, A6, A7, A5, Th5;

        end;

        hence thesis;

      end;

    end

    registration

      let n;

      cluster without_boundary for n -locally_euclidean non empty TopSpace;

      existence

      proof

        take M = ( Tball (( 0. ( TOP-REAL n)),1));

        thus thesis;

      end;

    end

    registration

      let n be non zero Nat;

      cluster with_boundary compact for n -locally_euclidean non empty TopSpace;

      existence

      proof

        take M = ( Tdisk (( 0. ( TOP-REAL n)),1));

        thus thesis;

      end;

    end

    registration

      let M be without_boundary locally_euclidean non empty TopSpace;

      cluster ( Fr M) -> empty;

      coherence

      proof

        ( Fr M) = (the carrier of M \ ( Int M)) by SUBSET_1:def 4

        .= (the carrier of M \ the carrier of M) by Def6

        .= {} by XBOOLE_1: 37;

        hence thesis;

      end;

    end

    registration

      let M be with_boundary locally_euclidean non empty TopSpace;

      cluster ( Fr M) -> non empty;

      coherence

      proof

        assume ( Fr M) is empty;

        then {} = (the carrier of M \ ( Int M)) by SUBSET_1:def 4;

        then the carrier of M c= ( Int M) by XBOOLE_1: 37;

        hence thesis by XBOOLE_0:def 10, Def6;

      end;

    end

    registration

      let n be zero Nat;

      cluster -> without_boundary for n -locally_euclidean non empty TopSpace;

      coherence

      proof

        set TR = ( TOP-REAL n), S = ( Sphere (( 0. TR),1));

        let M be n -locally_euclidean non empty TopSpace;

        assume M is with_boundary;

        then

        consider p be object such that

         A1: p in ( Fr M) by XBOOLE_0:def 1;

        reconsider p as Point of M by A1;

        consider U be a_neighborhood of p, m be Nat, h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL m)),1)) such that

         A2: h is being_homeomorphism and

         A3: (h . p) in ( Sphere (( 0. ( TOP-REAL m)),1)) by A1, Th5;

        

         A4: p in ( Int U) by CONNSP_2:def 1;

        consider W be a_neighborhood of p such that

         A5: ((M | W),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Def3;

        

         A6: p in ( Int W) by CONNSP_2:def 1;

        ((M | U),( Tdisk (( 0. ( TOP-REAL m)),1))) are_homeomorphic by A2, T_0TOPSP:def 1;

        then

        reconsider hp = (h . p) as Point of TR by A3, A6, A4, XBOOLE_0: 3, BROUWER3: 14, A5;

        hp = ( 0. TR) by A3;

        then |.( 0. TR).| = 1 by A3, TOPREAL9: 12;

        hence thesis;

      end;

    end

    theorem :: MFOLD_0:6

    M is without_boundary locally_euclidean non empty TopSpace iff for p be Point of M holds ex U be a_neighborhood of p, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Lm2;

    theorem :: MFOLD_0:7

    

     Th7: for M be with_boundary locally_euclidean non empty TopSpace holds for p be Point of M, n st ex U be a_neighborhood of p st ((M | U),( Tdisk (( 0. ( TOP-REAL (n + 1))),1))) are_homeomorphic holds for pF be Point of (M | ( Fr M)) st p = pF holds ex U be a_neighborhood of pF st (((M | ( Fr M)) | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic

    proof

      let M be with_boundary locally_euclidean non empty TopSpace;

      let p be Point of M, n such that

       A1: ex U be a_neighborhood of p st ((M | U),( Tdisk (( 0. ( TOP-REAL (n + 1))),1))) are_homeomorphic ;

      set n1 = (n + 1);

      set TR = ( TOP-REAL n1);

      consider W be a_neighborhood of p such that

       A2: ((M | W),( Tdisk (( 0. TR),1))) are_homeomorphic by A1;

      

       A3: p in ( Int W) by CONNSP_2:def 1;

      set TR1 = ( TOP-REAL n);

      set CL = ( cl_Ball (( 0. TR),1));

      set S = ( Sphere (( 0. TR),1));

      set F = ( Fr M), MF = (M | F);

      let pF be Point of MF such that

       A4: p = pF;

      

       A5: ( [#] MF) = F by PRE_TOPC:def 5;

      then

      consider U be a_neighborhood of p, m be Nat, h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL m)),1)) such that

       A6: h is being_homeomorphism and

       A7: (h . p) in ( Sphere (( 0. ( TOP-REAL m)),1)) by A4, Th5;

      

       A8: p in ( Int U) by CONNSP_2:def 1;

      ((M | U),( Tdisk (( 0. ( TOP-REAL m)),1))) are_homeomorphic by A6, T_0TOPSP:def 1;

      then

       A9: m = (n + 1) by A3, A8, XBOOLE_0: 3, A2, BROUWER3: 14;

      then

      reconsider h as Function of (M | U), ( Tdisk (( 0. TR),1));

      

       A10: ( Int U) c= U by TOPS_1: 16;

      ( [#] (M | U)) = U by PRE_TOPC:def 5;

      then

      reconsider IU = ( Int U) as Subset of (M | U) by TOPS_1: 16;

      set MU = (M | U);

      

       A11: pF in ( Int U) by A4, CONNSP_2:def 1;

      then p in (F /\ IU) by A4, A5, XBOOLE_0:def 4;

      then

      reconsider FIU = (F /\ ( Int U)) as non empty Subset of MU;

      

       A12: ( [#] (M | U)) = U by PRE_TOPC:def 5;

      IU is open by TSEP_1: 9;

      then (h .: IU) is open by A9, A6, TOPGRP_1: 25;

      then (h .: IU) in the topology of ( Tdisk (( 0. TR),1)) by PRE_TOPC:def 2;

      then

      consider W be Subset of TR such that

       A13: W in the topology of TR and

       A14: (h .: IU) = (W /\ ( [#] ( Tdisk (( 0. TR),1)))) by PRE_TOPC:def 4;

      reconsider W as open Subset of TR by A13, PRE_TOPC:def 2;

      

       A15: (h .: IU) = (W /\ CL) by PRE_TOPC:def 5, A14;

      

       A16: ( dom h) = ( [#] (M | U)) by A6, TOPS_2:def 5;

      then

       A17: (h . p) in (h .: IU) by A4, A11, FUNCT_1:def 6;

      then

      reconsider hp = (h . p) as Point of TR by A15;

      

       A18: ( Int W) = W by TOPS_1: 23;

      

       A19: |.(hp - ( 0. TR)).| = 1 by A9, A7, TOPREAL9: 9;

      reconsider HP = hp as Point of ( Euclid n1) by EUCLID: 67;

      (h . p) in W by A17, A14, XBOOLE_0:def 4;

      then

      consider s be Real such that

       A20: s > 0 and

       A21: ( Ball (HP,s)) c= W by A18, GOBOARD6: 5;

      set s2 = (s / 2), m = ( min ((s / 2),(1 / 2)));

      set V0 = (S /\ ( Ball (hp,m)));

      set hV0 = (h " V0);

      

       A22: m <= s2 by XXREAL_0: 17;

      s2 < s by A20, XREAL_1: 216;

      then

       A23: ( Ball (hp,m)) c= ( Ball (hp,s)) by A22, XXREAL_0: 2, JORDAN: 18;

      

       A24: ( Ball (HP,s)) = ( Ball (hp,s)) by TOPREAL9: 13;

      

       A25: hV0 c= F

      proof

        let x be object;

        assume

         A26: x in hV0;

        then

         A27: (h . x) in V0 by FUNCT_1:def 7;

        

         A28: x in ( dom h) by A26, FUNCT_1:def 7;

        then

        reconsider q = x as Point of M by A16, A12;

        reconsider hq = (h . q) as Point of TR by A27;

        (h . q) in ( Ball (hp,m)) by A27, XBOOLE_0:def 4;

        then

         A29: (h . q) in ( Ball (hp,s)) by A23;

        

         A30: (h . q) in ( Sphere (( 0. TR),1)) by A27, XBOOLE_0:def 4;

        then |.(hq - ( 0. TR)).| = 1 by TOPREAL9: 9;

        then hq in CL;

        then (h . q) in (h .: IU) by A15, A29, A21, A24, XBOOLE_0:def 4;

        then

        consider y be object such that

         A31: y in ( dom h) and

         A32: y in IU and

         A33: (h . y) = (h . q) by FUNCT_1:def 6;

        y = q by A6, A31, A33, A28, FUNCT_1:def 4;

        then U is a_neighborhood of q by A32, CONNSP_2:def 1;

        hence thesis by A9, A6, Th5, A30;

      end;

      reconsider FIU1 = FIU as Subset of MF by XBOOLE_1: 17, A5;

      ( Int U) in the topology of M by PRE_TOPC:def 2;

      then FIU1 in the topology of (M | F) by A5, PRE_TOPC:def 4;

      then

       A34: FIU1 is open by PRE_TOPC:def 2;

      

       A35: (MF | FIU1) = (M | (( Fr M) /\ ( Int U))) by XBOOLE_1: 17, PRE_TOPC: 7;

      set Mfiu = (MU | FIU);

      

       A36: (F /\ U) c= U by XBOOLE_1: 17;

      

       A37: ( [#] (TR | CL)) = CL by PRE_TOPC:def 5;

      then

      reconsider hFIU = (h .: FIU) as Subset of TR by XBOOLE_1: 1;

      

       A38: ( [#] (TR | hFIU)) = hFIU by PRE_TOPC:def 5;

      

       A39: (( Tdisk (( 0. TR),1)) | (h .: FIU)) = (TR | hFIU) by A37, PRE_TOPC: 7;

      then

      reconsider hfiu = (h | FIU) as Function of Mfiu, (TR | hFIU) by JORDAN24: 12;

      

       A40: hfiu is being_homeomorphism by A9, A6, METRIZTS: 2, A39;

      

       A41: ( Ball (( 0. TR1),1)) misses ( Sphere (( 0. TR1),1)) by TOPREAL9: 19;

      

       A42: S c= CL by TOPREAL9: 17;

      

       A43: IU = (h " (h .: IU)) by FUNCT_1: 82, A6, FUNCT_1: 76, A16;

      V0 c= ( Ball (hp,m)) by XBOOLE_1: 17;

      then

       A44: V0 c= W by A21, A23, A24;

      

       A45: V0 c= hFIU

      proof

        let x be object;

        assume

         A46: x in (S /\ ( Ball (hp,m)));

        then

        reconsider q = x as Point of TR;

        q in S by A46, XBOOLE_0:def 4;

        then q in (h .: IU) by A44, A46, A15, A42, XBOOLE_0:def 4;

        then

        consider w be object such that

         A47: w in ( dom h) and

         A48: w in IU and

         A49: (h . w) = q by FUNCT_1:def 6;

        reconsider w as Point of MU by A47;

        w in hV0 by A46, A47, A49, FUNCT_1:def 7;

        then w in FIU by A25, A48, XBOOLE_0:def 4;

        hence thesis by A47, A49, FUNCT_1:def 6;

      end;

      

       A50: V0 c= S by XBOOLE_1: 17;

      then V0 c= CL by A42;

      then V0 c= (h .: IU) by A44, A14, XBOOLE_1: 19, A37;

      then

       A51: hV0 c= IU by A43, RELAT_1: 143;

      

       A52: ( rng h) = ( [#] ( Tdisk (( 0. TR),1))) by A9, A6, TOPS_2:def 5;

      then (h .: (h " V0)) = V0 by FUNCT_1: 77, A42, A50, XBOOLE_1: 1, A37;

      then

       A53: (( Tdisk (( 0. TR),1)) | (h .: (h " V0))) = (TR | V0) by PRE_TOPC: 7, A42, A50, XBOOLE_1: 1;

      

       A54: CL = (S \/ ( Ball (( 0. TR),1))) by TOPREAL9: 18;

      

       A55: (hFIU /\ ( Ball (hp,m))) c= V0

      proof

        let x be object;

        assume

         A56: x in (hFIU /\ ( Ball (hp,m)));

        then

        reconsider q = x as Point of TR;

        

         A57: x in hFIU by A56, XBOOLE_0:def 4;

        

         A58: q in S

        proof

          reconsider Q = q as Point of ( Euclid n1) by EUCLID: 67;

          set WB = (W /\ ( Ball (( 0. TR),1)));

          

           A59: ( Int WB) = WB by TOPS_1: 23;

          hFIU c= (h .: IU) by XBOOLE_1: 17, RELAT_1: 123;

          then

           A60: q in W by A57, A14, XBOOLE_0:def 4;

          assume not q in S;

          then q in ( Ball (( 0. TR),1)) by A57, A37, A54, XBOOLE_0:def 3;

          then q in WB by A60, XBOOLE_0:def 4;

          then

          consider w be Real such that

           A61: w > 0 and

           A62: ( Ball (Q,w)) c= WB by A59, GOBOARD6: 5;

          set B = ( Ball (q,w));

          

           A63: ( Ball (Q,w)) = ( Ball (q,w)) by TOPREAL9: 13;

          consider u be object such that

           A64: u in ( dom h) and

           A65: u in FIU and

           A66: (h . u) = q by FUNCT_1:def 6, A57;

          reconsider u as Point of M by A65;

          

           A67: ( Ball (( 0. TR),1)) c= CL by A54, XBOOLE_1: 11;

          WB c= ( Ball (( 0. TR),1)) by XBOOLE_1: 17;

          then

           A68: B c= ( Ball (( 0. TR),1)) by A62, A63;

          then

          reconsider BB = B as Subset of ( Tdisk (( 0. TR),1)) by A67, XBOOLE_1: 1, A37;

          reconsider hBB = (h " BB) as Subset of M by A12, XBOOLE_1: 1;

          

           A69: B in the topology of TR by PRE_TOPC:def 2;

           |.(q - q).| = 0 by TOPRNS_1: 28;

          then q in BB by A61;

          then

           A70: u in hBB by A64, A66, FUNCT_1:def 7;

          (BB /\ CL) = BB by A67, XBOOLE_1: 1, A68, XBOOLE_1: 28;

          then BB in the topology of ( Tdisk (( 0. TR),1)) by A69, A37, PRE_TOPC:def 4;

          then BB is open by PRE_TOPC:def 2;

          then

           A72: (h " BB) is open by TOPGRP_1: 26, A9, A6;

          WB c= W by XBOOLE_1: 17;

          then BB c= W by A62, A63;

          then BB c= (h .: IU) by XBOOLE_1: 19, A14;

          then (h " BB) c= ( Int U) by RELAT_1: 143, A43;

          then hBB is open by A10, A12, A72, TSEP_1: 9;

          then

           A73: ( Int hBB) = hBB by TOPS_1: 23;

          

           A74: (( Tdisk (( 0. TR),1)) | BB) = (TR | ( Ball (q,w))) by A37, PRE_TOPC: 7;

          reconsider hBB as a_neighborhood of u by A73, A70, CONNSP_2:def 1;

          

           A75: (h .: hBB) = BB by FUNCT_1: 77, A52;

          

           A76: (MU | (h " BB)) = (M | hBB) by A12, PRE_TOPC: 7;

          then

          reconsider hB = (h | hBB) as Function of (M | hBB), (TR | ( Ball (q,w))) by JORDAN24: 12, A74, A75;

          hB is being_homeomorphism by A9, A6, A74, A75, A76, METRIZTS: 2;

          then

           A77: ((M | hBB),( Tball (q,w))) are_homeomorphic by T_0TOPSP:def 1;

          (( Tball (q,w)),( Tball (( 0. TR),1))) are_homeomorphic by A61, Th3;

          then ((M | hBB),( Tball (( 0. TR),1))) are_homeomorphic by A77, A61, BORSUK_3: 3;

          then

           A78: u in ( Int M) by Def4;

          u in F by A65, XBOOLE_0:def 4;

          then u in (( [#] M) \ ( Int M)) by SUBSET_1:def 4;

          hence thesis by XBOOLE_0:def 5, A78;

        end;

        x in ( Ball (hp,m)) by A56, XBOOLE_0:def 4;

        hence thesis by A58, XBOOLE_0:def 4;

      end;

      ((S /\ ( Ball (hp,m))) /\ ( Ball (hp,m))) = (S /\ (( Ball (hp,m)) /\ ( Ball (hp,m)))) by XBOOLE_1: 16

      .= V0;

      then

       A79: (hFIU /\ ( Ball (hp,m))) = V0 by A55, XBOOLE_1: 26, A45;

      reconsider v0 = V0 as Subset of (TR | hFIU) by A38, A45;

      ( Ball (hp,m)) in the topology of TR by PRE_TOPC:def 2;

      then v0 in the topology of (TR | hFIU) by A79, PRE_TOPC:def 4, A38;

      then

       A80: v0 is open by PRE_TOPC:def 2;

      

       A81: (( Ball (( 0. TR1),1)) \/ ( Sphere (( 0. TR1),1))) = ( cl_Ball (( 0. TR1),1)) by TOPREAL9: 18;

      

       A83: |.(hp - ( 0. TR)).| = |.(( 0. TR) - hp).| by TOPRNS_1: 27;

      

       A84: m > 0 by A20, XXREAL_0: 21;

      then

       A85: |.(( 0. TR) - hp).| < (1 + m) by A19, A83, XREAL_1: 29;

       |.(hp - hp).| = 0 by TOPRNS_1: 28;

      then hp in ( Ball (hp,m)) by A84;

      then

       A86: hp in V0 by A9, A7, XBOOLE_0:def 4;

      

       A87: pF in ( Int U) by A4, CONNSP_2:def 1;

      then

       A88: pF in hV0 by A16, A10, A12, A4, A86, FUNCT_1:def 7;

      m <= (1 / 2) by XXREAL_0: 17;

      then m < |.(( 0. TR) - hp).| by A19, A83, XXREAL_0: 2;

      then

      consider g be Function of (TR | (S /\ ( cl_Ball (hp,m)))), ( Tdisk (( 0. TR1),1)) such that

       A89: g is being_homeomorphism and

       A90: (g .: (S /\ ( Sphere (hp,m)))) = ( Sphere (( 0. TR1),1)) by A19, A83, A85, BROUWER3: 19;

      

       A91: ((g .: S) /\ (g .: ( Ball (hp,m)))) = (g .: V0) by A89, FUNCT_1: 62;

      

       A92: ( [#] Mfiu) = FIU by PRE_TOPC:def 5;

      then

      reconsider U0 = hV0 as non empty Subset of Mfiu by A51, A25, XBOOLE_1: 19, A16, A87, A4, A86, FUNCT_1:def 7;

      reconsider U0 = hV0 as Subset of Mfiu by A51, A25, XBOOLE_1: 19, A92;

      

       A93: ( [#] (MF | FIU1)) = FIU by PRE_TOPC:def 5;

      then

      reconsider u0 = U0 as Subset of (MF | FIU1) by A92;

      (hfiu " v0) = (FIU /\ U0) by FUNCT_1: 70;

      then (hfiu " v0) = U0 by A51, A25, XBOOLE_1: 19, XBOOLE_1: 28;

      then

       A94: U0 is open by A80, A40, TOPGRP_1: 26;

      reconsider FV0 = u0 as Subset of MF by XBOOLE_1: 1, A92;

      

       A95: (F /\ ( Int U)) c= (F /\ U) by XBOOLE_1: 26, TOPS_1: 16;

      then Mfiu = (M | (( Fr M) /\ ( Int U))) by A36, XBOOLE_1: 1, PRE_TOPC: 7;

      then FV0 is open by A34, A35, A94, TSEP_1: 9, A93;

      then pF in ( Int FV0) by A88, TOPS_1: 22;

      then

      reconsider FV0 as a_neighborhood of pF by CONNSP_2:def 1;

      reconsider MV0 = FV0 as Subset of M by A51, XBOOLE_1: 1;

      hV0 c= (IU /\ F) by A51, A25, XBOOLE_1: 19;

      then FV0 c= (F /\ U) by A95;

      then

       A96: (MU | (h " V0)) = (M | MV0) by PRE_TOPC: 7, A36, XBOOLE_1: 1;

      (S /\ ( Sphere (hp,m))) misses V0 by TOPREAL9: 19, XBOOLE_1: 76;

      then

       A97: ( Sphere (( 0. ( TOP-REAL n)),1)) misses (g .: V0) by A89, A90, FUNCT_1: 66;

      

       A98: ((g .: S) /\ (g .: ( Sphere (hp,m)))) = (g .: (S /\ ( Sphere (hp,m)))) by A89, FUNCT_1: 62;

      

       A99: ( [#] (TR | (S /\ ( cl_Ball (hp,m))))) = (S /\ ( cl_Ball (hp,m))) by PRE_TOPC:def 5;

      then

       A100: ( dom g) = (S /\ ( cl_Ball (hp,m))) by A89, TOPS_2:def 5;

      

       A101: (( Ball (hp,m)) \/ ( Sphere (hp,m))) = ( cl_Ball (hp,m)) by TOPREAL9: 18;

      then

      reconsider ZV0 = V0 as Subset of (TR | (S /\ ( cl_Ball (hp,m)))) by XBOOLE_1: 7, XBOOLE_1: 26, A99;

      

       A102: (g .: ( cl_Ball (hp,m))) = ((g .: ( Ball (hp,m))) \/ (g .: ( Sphere (hp,m)))) by A101, RELAT_1: 120;

      

       A103: ( [#] ( Tdisk (( 0. TR1),1))) = ( cl_Ball (( 0. TR1),1)) by PRE_TOPC:def 5;

      then ( rng g) = ( cl_Ball (( 0. TR1),1)) by A89, TOPS_2:def 5;

      

      then ( cl_Ball (( 0. TR1),1)) = (g .: (S /\ ( cl_Ball (hp,m)))) by A100, RELAT_1: 113

      .= ((g .: S) /\ (g .: ( cl_Ball (hp,m)))) by A89, FUNCT_1: 62

      .= ((g .: V0) \/ ( Sphere (( 0. ( TOP-REAL n)),1))) by A102, A98, A91, A90, XBOOLE_1: 23;

      then (g .: V0) = ( Ball (( 0. TR1),1)) by A81, A41, A97, XBOOLE_1: 71;

      then

       A104: (( Tdisk (( 0. TR1),1)) | (g .: ZV0)) = ( Tball (( 0. TR1),1)) by PRE_TOPC: 7, A103;

      

       A105: ((TR | (S /\ ( cl_Ball (hp,m)))) | ZV0) = (TR | V0) by A99, PRE_TOPC: 7;

      then

      reconsider GG = (g | ZV0) as Function of (TR | V0), ( Tball (( 0. TR1),1)) by A86, JORDAN24: 12, A104;

      

       A106: GG is being_homeomorphism by A89, METRIZTS: 2, A105, A104;

      

       A107: (M | MV0) = (MF | FV0) by A5, PRE_TOPC: 7;

      then

      reconsider HH = (h | FV0) as Function of (MF | FV0), (TR | V0) by A96, A53, JORDAN24: 12;

      reconsider GH = (GG * HH) as Function of (MF | FV0), ( Tball (( 0. TR1),1)) by A86;

      take FV0;

      HH is being_homeomorphism by A9, A6, METRIZTS: 2, A96, A53, A107;

      then GH is being_homeomorphism by A86, A106, TOPS_2: 57;

      hence thesis by T_0TOPSP:def 1;

    end;

    

     Lm4: for M be locally_euclidean non empty TopSpace holds for p be Point of (M | ( Int M)) holds ex U be a_neighborhood of p, n st (((M | ( Int M)) | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic

    proof

      let M be locally_euclidean non empty TopSpace;

      set MI = (M | ( Int M));

      let p be Point of (M | ( Int M));

      

       A1: ( [#] MI) = ( Int M) by PRE_TOPC:def 5;

      then p in ( Int M);

      then

      reconsider q = p as Point of M;

      consider U be a_neighborhood of q, n such that

       A2: ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A1, Def4;

      

       A3: ( Int U) c= U by TOPS_1: 16;

      

       A4: (( Int M) /\ ( Int U)) in the topology of M by PRE_TOPC:def 2;

      

       A5: ( Int U) c= U by TOPS_1: 16;

      set MU = (M | U), TR = ( TOP-REAL n);

      consider h be Function of MU, ( Tball (( 0. TR),1)) such that

       A6: h is being_homeomorphism by A2, T_0TOPSP:def 1;

      

       A7: ( [#] MU) = U by PRE_TOPC:def 5;

      (( Int U) /\ ( Int M)) c= ( Int U) by XBOOLE_1: 17;

      then

      reconsider UIM = (( Int M) /\ ( Int U)) as Subset of MU by A5, A7, XBOOLE_1: 1;

      

       A8: ( dom h) = ( [#] MU) by A6, TOPS_2:def 5;

      

       A10: ( [#] ( Tball (( 0. TR),1))) = ( Ball (( 0. TR),1)) by PRE_TOPC:def 5;

      then

      reconsider hum = (h .: UIM) as Subset of TR by XBOOLE_1: 1;

      (UIM /\ ( [#] MU)) = UIM by XBOOLE_1: 28;

      then UIM in the topology of MU by A4, PRE_TOPC:def 4;

      then UIM is open by PRE_TOPC:def 2;

      then (h .: UIM) is open by A6, TOPGRP_1: 25;

      then hum is open by TSEP_1: 9, A10;

      then

       A11: ( Int hum) = hum by TOPS_1: 23;

      

       A12: (h " (h .: UIM)) c= UIM by A6, FUNCT_1: 82;

      

       A13: q in ( Int U) by CONNSP_2:def 1;

      then

       A14: q in UIM by A1, XBOOLE_0:def 4;

      then (h . q) in hum by A8, FUNCT_1:def 6;

      then

      reconsider hq = (h . q) as Point of TR;

      reconsider HQ = hq as Point of ( Euclid n) by EUCLID: 67;

      (h . q) in (h .: UIM) by A14, A8, FUNCT_1:def 6;

      then

      consider s be Real such that

       A15: s > 0 and

       A16: ( Ball (HQ,s)) c= hum by A11, GOBOARD6: 5;

      

       A17: ( Ball (HQ,s)) = ( Ball (hq,s)) by TOPREAL9: 13;

      then

      reconsider BB = ( Ball (hq,s)) as Subset of ( Tball (( 0. TR),1)) by A16, XBOOLE_1: 1;

      BB is open by TSEP_1: 9;

      then

      reconsider hBB = (h " BB) as open Subset of MU by A6, TOPGRP_1: 26;

      hBB c= (h " (h .: UIM)) by A16, A17, RELAT_1: 143;

      then

       A18: hBB c= UIM by A12;

      reconsider hBBM = hBB as Subset of M by A7, XBOOLE_1: 1;

      (( Int U) /\ ( Int M)) c= ( Int M) by XBOOLE_1: 17;

      then

      reconsider HBB = hBBM as Subset of MI by A18, XBOOLE_1: 1, A1;

      hBBM is open by TSEP_1: 9, A18;

      then

       A19: HBB is open by TSEP_1: 9;

      

       A20: (M | hBBM) = (MI | HBB) by A1, PRE_TOPC: 7;

      ( rng h) = ( [#] ( Tball (( 0. TR),1))) by A6, TOPS_2:def 5;

      then (h .: hBB) = BB by FUNCT_1: 77;

      then

       A21: (( Tball (( 0. TR),1)) | (h .: hBB)) = (TR | ( Ball (hq,s))) by A10, PRE_TOPC: 7;

       |.(hq - hq).| = 0 by TOPRNS_1: 28;

      then hq in BB by A15;

      then p in HBB by FUNCT_1:def 7, A13, A3, A8, A7;

      then p in ( Int HBB) by A19, TOPS_1: 23;

      then

      reconsider HBB as a_neighborhood of p by CONNSP_2:def 1;

      

       A22: (MU | hBB) = (M | hBBM) by A7, PRE_TOPC: 7;

      then

      reconsider hh = (h | hBB) as Function of (MI | HBB), (TR | ( Ball (hq,s))) by A21, JORDAN24: 12, A20;

      hh is being_homeomorphism by A6, A21, A22, A20, METRIZTS: 2;

      then

       A23: ((MI | HBB),( Tball (hq,s))) are_homeomorphic by T_0TOPSP:def 1;

      take HBB;

      (( Tball (hq,s)),( Tball (( 0. TR),1))) are_homeomorphic by A15, Th3;

      hence thesis by A15, A23, BORSUK_3: 3;

    end;

    registration

      let M be locally_euclidean non empty TopSpace;

      cluster (M | ( Int M)) -> locally_euclidean;

      coherence

      proof

        for p be Point of (M | ( Int M)) holds ex U be a_neighborhood of p, n st (((M | ( Int M)) | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Lm4;

        hence thesis by Lm2;

      end;

      cluster (M | ( Int M)) -> without_boundary;

      coherence

      proof

        for p be Point of (M | ( Int M)) holds ex U be a_neighborhood of p, n st (((M | ( Int M)) | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Lm4;

        hence thesis by Lm2;

      end;

    end

    

     Lm5: for M be with_boundary locally_euclidean non empty TopSpace holds for p be Point of M holds for pM be Point of (M | ( Fr M)) st p = pM holds for U be a_neighborhood of p, n be Nat, h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL n)),1)) st h is being_homeomorphism & (h . p) in ( Sphere (( 0. ( TOP-REAL n)),1)) holds ex n1 be Nat, U be a_neighborhood of pM st (n1 + 1) = n & (((M | ( Fr M)) | U),( Tball (( 0. ( TOP-REAL n1)),1))) are_homeomorphic

    proof

      let M be with_boundary locally_euclidean non empty TopSpace;

      let p be Point of M;

      let pM be Point of (M | ( Fr M)) such that

       A1: p = pM;

      let U be a_neighborhood of p;

      let n be Nat;

      let h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL n)),1)) such that

       A2: h is being_homeomorphism and

       A3: (h . p) in ( Sphere (( 0. ( TOP-REAL n)),1));

      set TR = ( TOP-REAL n);

      n > 0

      proof

        assume n <= 0 ;

        then n = 0 ;

        then (h . p) = ( 0. TR) by A3, JORDAN2C: 105;

        then |.( 0. TR).| = 1 by A3, TOPREAL9: 12;

        hence thesis by EUCLID_2: 42;

      end;

      then

      reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20;

      take n1;

      ((M | U),( Tdisk (( 0. ( TOP-REAL (n1 + 1))),1))) are_homeomorphic by A2, T_0TOPSP:def 1;

      then ex U be a_neighborhood of pM st (((M | ( Fr M)) | U),( Tball (( 0. ( TOP-REAL n1)),1))) are_homeomorphic by Th7, A1;

      hence thesis;

    end;

    registration

      let M be with_boundary locally_euclidean non empty TopSpace;

      cluster (M | ( Fr M)) -> locally_euclidean;

      coherence

      proof

        set MF = (M | ( Fr M));

        now

          let pM be Point of MF;

          

           A1: ( [#] MF) = ( Fr M) by PRE_TOPC:def 5;

          then pM in ( Fr M);

          then

          reconsider p = pM as Point of M;

          consider U be a_neighborhood of p, n be Nat, h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL n)),1)) such that

           A2: h is being_homeomorphism and

           A3: (h . p) in ( Sphere (( 0. ( TOP-REAL n)),1)) by Th5, A1;

          ex n1 be Nat, U be a_neighborhood of pM st (n1 + 1) = n & (((M | ( Fr M)) | U),( Tball (( 0. ( TOP-REAL n1)),1))) are_homeomorphic by Lm5, A2, A3;

          hence ex U be a_neighborhood of pM, n1 be Nat st (((M | ( Fr M)) | U),( Tball (( 0. ( TOP-REAL n1)),1))) are_homeomorphic ;

        end;

        hence thesis by Lm2;

      end;

      cluster (M | ( Fr M)) -> without_boundary;

      coherence

      proof

        set MF = (M | ( Fr M));

        now

          let pM be Point of MF;

          

           A4: ( [#] MF) = ( Fr M) by PRE_TOPC:def 5;

          then pM in ( Fr M);

          then

          reconsider p = pM as Point of M;

          consider U be a_neighborhood of p, n be Nat, h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL n)),1)) such that

           A5: h is being_homeomorphism and

           A6: (h . p) in ( Sphere (( 0. ( TOP-REAL n)),1)) by Th5, A4;

          ex n1 be Nat, U be a_neighborhood of pM st (n1 + 1) = n & (((M | ( Fr M)) | U),( Tball (( 0. ( TOP-REAL n1)),1))) are_homeomorphic by Lm5, A5, A6;

          hence ex U be a_neighborhood of pM, n1 be Nat st (((M | ( Fr M)) | U),( Tball (( 0. ( TOP-REAL n1)),1))) are_homeomorphic ;

        end;

        hence thesis by Lm2;

      end;

    end

    begin

    registration

      let N,M be locally_euclidean non empty TopSpace;

      cluster [:N, M:] -> locally_euclidean;

      coherence

      proof

        let p be Point of [:N, M:];

        p in the carrier of [:N, M:];

        then p in [:the carrier of N, the carrier of M:] by BORSUK_1:def 2;

        then

        consider x,y be object such that

         A1: x in the carrier of N and

         A2: y in the carrier of M and

         A3: p = [x, y] by ZFMISC_1:def 2;

        reconsider x as Point of N by A1;

        consider Ux be a_neighborhood of x, n such that

         A4: ((N | Ux),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Def2;

        reconsider y as Point of M by A2;

        consider Uy be a_neighborhood of y, m such that

         A5: ((M | Uy),( Tdisk (( 0. ( TOP-REAL m)),1))) are_homeomorphic by Def2;

        consider hy be Function of (M | Uy), ( Tdisk (( 0. ( TOP-REAL m)),1)) such that

         A6: hy is being_homeomorphism by A5, T_0TOPSP:def 1;

        consider hx be Function of (N | Ux), ( Tdisk (( 0. ( TOP-REAL n)),1)) such that

         A7: hx is being_homeomorphism by A4, T_0TOPSP:def 1;

         [:hx, hy:] is being_homeomorphism by A6, TIETZE_2: 15, A7;

        then

         A8: ( [:(N | Ux), (M | Uy):], [:( Tdisk (( 0. ( TOP-REAL n)),1)), ( Tdisk (( 0. ( TOP-REAL m)),1)):]) are_homeomorphic by T_0TOPSP:def 1;

        reconsider mn = (m + n) as Nat;

        ex hf be Function of [:( Tdisk (( 0. ( TOP-REAL n)),1)), ( Tdisk (( 0. ( TOP-REAL m)),1)):], ( Tdisk (( 0. ( TOP-REAL mn)),1)) st hf is being_homeomorphism & (hf .: [:( Ball (( 0. ( TOP-REAL n)),1)), ( Ball (( 0. ( TOP-REAL m)),1)):]) = ( Ball (( 0. ( TOP-REAL mn)),1)) by TIETZE_2: 19;

        then

         A9: ( [:( Tdisk (( 0. ( TOP-REAL n)),1)), ( Tdisk (( 0. ( TOP-REAL m)),1)):],( Tdisk (( 0. ( TOP-REAL mn)),1))) are_homeomorphic by T_0TOPSP:def 1;

         [:(N | Ux), (M | Uy):] = ( [:N, M:] | [:Ux, Uy:]) by BORSUK_3: 22;

        hence thesis by A9, A8, BORSUK_3: 3, A3;

      end;

    end

    theorem :: MFOLD_0:8

    

     Th8: for N,M be locally_euclidean non empty TopSpace holds ( Int [:N, M:]) = [:( Int N), ( Int M):]

    proof

      let N,M be locally_euclidean non empty TopSpace;

      set NM = [:N, M:], IN = ( Int N), IM = ( Int M);

      thus ( Int NM) c= [:IN, IM:]

      proof

        let z be object;

        assume

         A1: z in ( Int NM);

        then

        reconsider p = z as Point of NM;

        z in the carrier of NM by A1;

        then z in [:the carrier of N, the carrier of M:] by BORSUK_1:def 2;

        then

        consider x,y be object such that

         A2: x in the carrier of N and

         A3: y in the carrier of M and

         A4: z = [x, y] by ZFMISC_1:def 2;

        reconsider y as Point of M by A3;

        reconsider x as Point of N by A2;

        assume

         A5: not z in [:IN, IM:];

        per cases by A5, A4, ZFMISC_1: 87;

          suppose

           A6: not x in IN;

          consider W be a_neighborhood of y, m be Nat such that

           A7: ((M | W),( Tdisk (( 0. ( TOP-REAL m)),1))) are_homeomorphic by Def2;

          x in (( [#] N) \ IN) by A6, XBOOLE_0:def 5;

          then x in ( Fr N) by SUBSET_1:def 4;

          then

          consider U be a_neighborhood of x, n be Nat, h be Function of (N | U), ( Tdisk (( 0. ( TOP-REAL n)),1)) such that

           A8: h is being_homeomorphism and

           A9: (h . x) in ( Sphere (( 0. ( TOP-REAL n)),1)) by Th5;

          

           A10: y in ( Int W) by CONNSP_2:def 1;

          reconsider mn = (m + n) as Nat;

          set TRm = ( TOP-REAL m), TRn = ( TOP-REAL n), TRnm = ( TOP-REAL mn);

          consider f be Function of (M | W), ( Tdisk (( 0. TRm),1)) such that

           A11: f is being_homeomorphism by A7, T_0TOPSP:def 1;

          

           A12: not (h . x) in ( Ball (( 0. TRn),1)) by TOPREAL9: 19, A9, XBOOLE_0: 3;

          consider hf be Function of [:( Tdisk (( 0. TRn),1)), ( Tdisk (( 0. TRm),1)):], ( Tdisk (( 0. TRnm),1)) such that

           A13: hf is being_homeomorphism and

           A14: (hf .: [:( Ball (( 0. TRn),1)), ( Ball (( 0. TRm),1)):]) = ( Ball (( 0. TRnm),1)) by TIETZE_2: 19;

          set H = (hf * [:h, f:]);

           [:h, f:] is being_homeomorphism by A8, A11, TIETZE_2: 15;

          then

           A15: H is being_homeomorphism by A13, TOPS_2: 57;

          then

           A16: ( rng H) = ( [#] ( Tdisk (( 0. TRnm),1))) by TOPS_2:def 5;

          

           A17: ( Int W) c= W by TOPS_1: 16;

          

           A18: ( Int U) c= U by TOPS_1: 16;

          x in ( Int U) by CONNSP_2:def 1;

          then

           A19: [x, y] in [:U, W:] by A18, A17, A10, ZFMISC_1: 87;

          (n + m) in NAT by ORDINAL1:def 12;

          then

           A20: ( [#] ( Tdisk (( 0. TRnm),1))) = ( cl_Ball (( 0. TRnm),1)) by BROUWER: 3;

          

           A21: [:(N | U), (M | W):] = (NM | [:U, W:]) by BORSUK_3: 22;

          then ( dom H) = ( [#] (NM | [:U, W:])) by A15, TOPS_2:def 5;

          then

           A22: p in ( dom H) by A19, A4, PRE_TOPC:def 5;

          then

           A23: ( [:h, f:] . p) in ( dom hf) by FUNCT_1: 11;

          ( dom [:h, f:]) = [:( dom h), ( dom f):] by FUNCT_3:def 8;

          then

           A24: ( [:h, f:] . (x,y)) = [(h . x), (f . y)] by A22, FUNCT_1: 11, A4, FUNCT_3: 65;

          

           A25: (H . p) = (hf . ( [:h, f:] . p)) by A22, FUNCT_1: 12;

          (H . p) in ( Sphere (( 0. TRnm),1))

          proof

            (H . p) in ( cl_Ball (( 0. TRnm),1)) by A16, A20, A22, FUNCT_1:def 3;

            then

             A26: (H . p) in (( Sphere (( 0. TRnm),1)) \/ ( Ball (( 0. TRnm),1))) by TOPREAL9: 18;

            assume not (H . p) in ( Sphere (( 0. TRnm),1));

            then (H . p) in (hf .: [:( Ball (( 0. TRn),1)), ( Ball (( 0. TRm),1)):]) by A26, XBOOLE_0:def 3, A14;

            then

            consider w be object such that

             A27: w in ( dom hf) and

             A28: w in [:( Ball (( 0. TRn),1)), ( Ball (( 0. TRm),1)):] and

             A29: (hf . w) = (H . p) by FUNCT_1:def 6;

            w = ( [:h, f:] . p) by A25, A23, A13, A27, A29, FUNCT_1:def 4;

            hence thesis by A28, A4, A24, A12, ZFMISC_1: 87;

          end;

          then p in ( Fr NM) by A21, A4, Th5, A15;

          then p in (( [#] NM) \ ( Int NM)) by SUBSET_1:def 4;

          hence thesis by XBOOLE_0:def 5, A1;

        end;

          suppose not y in IM;

          then y in (( [#] M) \ IM) by XBOOLE_0:def 5;

          then y in ( Fr M) by SUBSET_1:def 4;

          then

          consider W be a_neighborhood of y, m be Nat, f be Function of (M | W), ( Tdisk (( 0. ( TOP-REAL m)),1)) such that

           A30: f is being_homeomorphism and

           A31: (f . y) in ( Sphere (( 0. ( TOP-REAL m)),1)) by Th5;

          

           A32: y in ( Int W) by CONNSP_2:def 1;

          consider U be a_neighborhood of x, n be Nat such that

           A33: ((N | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Def2;

          reconsider mn = (n + m) as Nat;

          set TRm = ( TOP-REAL m), TRn = ( TOP-REAL n), TRnm = ( TOP-REAL mn);

          consider h be Function of (N | U), ( Tdisk (( 0. TRn),1)) such that

           A34: h is being_homeomorphism by A33, T_0TOPSP:def 1;

          

           A35: not (f . y) in ( Ball (( 0. TRm),1)) by TOPREAL9: 19, A31, XBOOLE_0: 3;

          consider hf be Function of [:( Tdisk (( 0. TRn),1)), ( Tdisk (( 0. TRm),1)):], ( Tdisk (( 0. TRnm),1)) such that

           A36: hf is being_homeomorphism and

           A37: (hf .: [:( Ball (( 0. TRn),1)), ( Ball (( 0. TRm),1)):]) = ( Ball (( 0. TRnm),1)) by TIETZE_2: 19;

          set H = (hf * [:h, f:]);

           [:h, f:] is being_homeomorphism by A30, A34, TIETZE_2: 15;

          then

           A38: H is being_homeomorphism by A36, TOPS_2: 57;

          then

           A39: ( rng H) = ( [#] ( Tdisk (( 0. TRnm),1))) by TOPS_2:def 5;

          

           A40: ( Int W) c= W by TOPS_1: 16;

          

           A41: ( Int U) c= U by TOPS_1: 16;

          x in ( Int U) by CONNSP_2:def 1;

          then

           A42: [x, y] in [:U, W:] by A41, A40, A32, ZFMISC_1: 87;

          (n + m) in NAT by ORDINAL1:def 12;

          then

           A43: ( [#] ( Tdisk (( 0. TRnm),1))) = ( cl_Ball (( 0. TRnm),1)) by BROUWER: 3;

          

           A44: [:(N | U), (M | W):] = (NM | [:U, W:]) by BORSUK_3: 22;

          then ( dom H) = ( [#] (NM | [:U, W:])) by A38, TOPS_2:def 5;

          then

           A45: p in ( dom H) by A42, A4, PRE_TOPC:def 5;

          then

           A46: ( [:h, f:] . p) in ( dom hf) by FUNCT_1: 11;

          ( dom [:h, f:]) = [:( dom h), ( dom f):] by FUNCT_3:def 8;

          then

           A47: ( [:h, f:] . (x,y)) = [(h . x), (f . y)] by A45, FUNCT_1: 11, A4, FUNCT_3: 65;

          

           A48: (H . p) = (hf . ( [:h, f:] . p)) by A45, FUNCT_1: 12;

          (H . p) in ( Sphere (( 0. TRnm),1))

          proof

            (H . p) in ( cl_Ball (( 0. TRnm),1)) by A39, A43, A45, FUNCT_1:def 3;

            then

             A49: (H . p) in (( Sphere (( 0. TRnm),1)) \/ ( Ball (( 0. TRnm),1))) by TOPREAL9: 18;

            assume not (H . p) in ( Sphere (( 0. TRnm),1));

            then (H . p) in (hf .: [:( Ball (( 0. TRn),1)), ( Ball (( 0. TRm),1)):]) by A49, XBOOLE_0:def 3, A37;

            then

            consider w be object such that

             A50: w in ( dom hf) and

             A51: w in [:( Ball (( 0. TRn),1)), ( Ball (( 0. TRm),1)):] and

             A52: (hf . w) = (H . p) by FUNCT_1:def 6;

            w = ( [:h, f:] . p) by A48, A46, A36, A50, A52, FUNCT_1:def 4;

            hence thesis by A51, A4, A47, A35, ZFMISC_1: 87;

          end;

          then p in ( Fr NM) by A44, A4, Th5, A38;

          then p in (( [#] NM) \ ( Int NM)) by SUBSET_1:def 4;

          hence thesis by XBOOLE_0:def 5, A1;

        end;

      end;

      let z be object;

      assume

       A53: z in [:IN, IM:];

      then

      consider x,y be object such that

       A54: x in IN and

       A55: y in IM and

       A56: z = [x, y] by ZFMISC_1:def 2;

      reconsider x as Point of N by A54;

      consider U be a_neighborhood of x, n such that

       A57: ((N | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A54, Def4;

      reconsider y as Point of M by A55;

      consider W be a_neighborhood of y, m such that

       A58: ((M | W),( Tball (( 0. ( TOP-REAL m)),1))) are_homeomorphic by A55, Def4;

      reconsider p = z as Point of NM by A53;

      set TRn = ( TOP-REAL n), TRm = ( TOP-REAL m);

      reconsider mn = (m + n) as Nat;

      ( [:(N | U), (M | W):],(( TOP-REAL mn) | ( Ball (( 0. ( TOP-REAL mn)),1)))) are_homeomorphic by A57, A58, TIETZE_2: 20;

      then ((NM | [:U, W:]),( Tball (( 0. ( TOP-REAL mn)),1))) are_homeomorphic by BORSUK_3: 22;

      hence thesis by Def4, A56;

    end;

    theorem :: MFOLD_0:9

    

     Th9: for N,M be locally_euclidean non empty TopSpace holds ( Fr [:N, M:]) = ( [:( [#] N), ( Fr M):] \/ [:( Fr N), ( [#] M):])

    proof

      let N,M be locally_euclidean non empty TopSpace;

      

      thus ( Fr [:N, M:]) = (( [#] [:N, M:]) \ ( Int [:N, M:])) by SUBSET_1:def 4

      .= ( [:( [#] N), ( [#] M):] \ ( Int [:N, M:])) by BORSUK_1:def 2

      .= ( [:( [#] N), ( [#] M):] \ [:( Int N), ( Int M):]) by Th8

      .= ( [:(( [#] N) \ ( Int N)), ( [#] M):] \/ [:( [#] N), (( [#] M) \ ( Int M)):]) by ZFMISC_1: 103

      .= ( [:(( [#] N) \ ( Int N)), ( [#] M):] \/ [:( [#] N), ( Fr M):]) by SUBSET_1:def 4

      .= ( [:( [#] N), ( Fr M):] \/ [:( Fr N), ( [#] M):]) by SUBSET_1:def 4;

    end;

    registration

      let N,M be without_boundary locally_euclidean non empty TopSpace;

      cluster [:N, M:] -> without_boundary;

      coherence

      proof

        ( Int [:N, M:]) = [:( Int N), ( Int M):] by Th8

        .= [:the carrier of N, ( Int M):] by Def6

        .= [:the carrier of N, the carrier of M:] by Def6

        .= the carrier of [:N, M:] by BORSUK_1:def 2;

        hence thesis;

      end;

    end

    registration

      let N be locally_euclidean non empty TopSpace;

      let M be with_boundary locally_euclidean non empty TopSpace;

      cluster [:N, M:] -> with_boundary;

      coherence

      proof

        ( Fr [:N, M:]) = ( [:( [#] N), ( Fr M):] \/ [:( Fr N), ( [#] M):]) by Th9;

        hence thesis;

      end;

      cluster [:M, N:] -> with_boundary;

      coherence

      proof

        ( Fr [:M, N:]) = ( [:( [#] M), ( Fr N):] \/ [:( Fr M), ( [#] N):]) by Th9;

        hence thesis;

      end;

    end

    begin

    definition

      let n;

      let M be n -locally_euclidean non empty TopSpace;

      :: original: Int

      redefine

      :: MFOLD_0:def7

      func Int M -> Subset of M means

      : Def7: for p be Point of M holds p in it iff ex U be a_neighborhood of p st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

      compatibility

      proof

        let I be Subset of M;

        thus I = ( Int M) implies for p be Point of M holds p in I iff ex U be a_neighborhood of p st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic

        proof

          assume

           A1: I = ( Int M);

          let p be Point of M;

          thus p in I implies ex U be a_neighborhood of p st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic

          proof

            consider W be a_neighborhood of p such that

             A2: ((M | W),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Def3;

            

             A3: p in ( Int W) by CONNSP_2:def 1;

            assume p in I;

            then

            consider U be a_neighborhood of p, m such that

             A4: ((M | U),( Tball (( 0. ( TOP-REAL m)),1))) are_homeomorphic by A1, Def4;

            p in ( Int U) by CONNSP_2:def 1;

            then n = m by A3, XBOOLE_0: 3, A4, A2, BROUWER3: 15;

            hence thesis by A4;

          end;

          thus thesis by Def4, A1;

        end;

        assume

         A6: for p be Point of M holds p in I iff ex U be a_neighborhood of p st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

        thus I c= ( Int M)

        proof

          let x be object;

          assume

           A7: x in I;

          then

          reconsider x as Point of M;

          ex U be a_neighborhood of x st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A7, A6;

          hence thesis by Def4;

        end;

        let x be object;

        assume

         A8: x in ( Int M);

        then

        reconsider x as Point of M;

        consider U be a_neighborhood of x, m such that

         A9: ((M | U),( Tball (( 0. ( TOP-REAL m)),1))) are_homeomorphic by A8, Def4;

        consider W be a_neighborhood of x such that

         A11: ((M | W),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Def3;

        

         A12: x in ( Int W) by CONNSP_2:def 1;

        x in ( Int U) by CONNSP_2:def 1;

        then m = n by A12, XBOOLE_0: 3, BROUWER3: 15, A9, A11;

        hence thesis by A6, A9;

      end;

      coherence ;

    end

    definition

      let n;

      let M be n -locally_euclidean non empty TopSpace;

      :: original: Fr

      redefine

      :: MFOLD_0:def8

      func Fr M -> Subset of M means for p be Point of M holds p in it iff ex U be a_neighborhood of p, h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL n)),1)) st h is being_homeomorphism & (h . p) in ( Sphere (( 0. ( TOP-REAL n)),1));

      compatibility

      proof

        set TR = ( TOP-REAL n);

        let F be Subset of M;

        thus F = ( Fr M) implies for p be Point of M holds p in F iff ex U be a_neighborhood of p, h be Function of (M | U), ( Tdisk (( 0. TR),1)) st h is being_homeomorphism & (h . p) in ( Sphere (( 0. TR),1))

        proof

          assume

           A1: F = ( Fr M);

          let p be Point of M;

          thus p in F implies ex U be a_neighborhood of p, h be Function of (M | U), ( Tdisk (( 0. TR),1)) st h is being_homeomorphism & (h . p) in ( Sphere (( 0. TR),1))

          proof

            consider W be a_neighborhood of p such that

             A2: ((M | W),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Def3;

            

             A3: p in ( Int W) by CONNSP_2:def 1;

            assume p in F;

            then

            consider U be a_neighborhood of p, m be Nat, h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL m)),1)) such that

             A4: h is being_homeomorphism and

             A5: (h . p) in ( Sphere (( 0. ( TOP-REAL m)),1)) by A1, Th5;

            

             A6: p in ( Int U) by CONNSP_2:def 1;

            ((M | U),( Tdisk (( 0. ( TOP-REAL m)),1))) are_homeomorphic by A4, T_0TOPSP:def 1;

            then n = m by A3, A6, XBOOLE_0: 3, A2, BROUWER3: 14;

            hence thesis by A4, A5;

          end;

          thus thesis by Th5, A1;

        end;

        assume

         A7: for p be Point of M holds p in F iff ex U be a_neighborhood of p, h be Function of (M | U), ( Tdisk (( 0. TR),1)) st h is being_homeomorphism & (h . p) in ( Sphere (( 0. TR),1));

        thus F c= ( Fr M)

        proof

          let x be object;

          assume

           A8: x in F;

          then

          reconsider x as Point of M;

          ex U be a_neighborhood of x, h be Function of (M | U), ( Tdisk (( 0. TR),1)) st h is being_homeomorphism & (h . x) in ( Sphere (( 0. TR),1)) by A8, A7;

          hence thesis by Th5;

        end;

        let x be object;

        assume

         A9: x in ( Fr M);

        then

        reconsider x as Point of M;

        consider U be a_neighborhood of x, m be Nat, h be Function of (M | U), ( Tdisk (( 0. ( TOP-REAL m)),1)) such that

         A10: h is being_homeomorphism and

         A11: (h . x) in ( Sphere (( 0. ( TOP-REAL m)),1)) by A9, Th5;

        

         A12: x in ( Int U) by CONNSP_2:def 1;

        consider W be a_neighborhood of x such that

         A13: ((M | W),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Def3;

        

         A14: x in ( Int W) by CONNSP_2:def 1;

        ((M | U),( Tdisk (( 0. ( TOP-REAL m)),1))) are_homeomorphic by A10, T_0TOPSP:def 1;

        then n = m by A14, A12, XBOOLE_0: 3, A13, BROUWER3: 14;

        hence thesis by A10, A11, A7;

      end;

      coherence ;

    end

    theorem :: MFOLD_0:10

    M1 is locally_euclidean & (M1,M2) are_homeomorphic implies M2 is locally_euclidean

    proof

      assume that

       A1: M1 is locally_euclidean and

       A2: (M1,M2) are_homeomorphic ;

      let p be Point of M2;

      consider h be Function of M2, M1 such that

       A3: h is being_homeomorphism by A2, T_0TOPSP:def 1;

      reconsider hp = (h . p) as Point of M1;

      consider U be a_neighborhood of hp, n such that

       A4: ((M1 | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A1;

      

       A5: ( rng h) = ( [#] M1) by A3, TOPS_2:def 5;

      then

       A6: (h .: (h " U)) = U by FUNCT_1: 77;

      then

      reconsider hhU = (h | (h " U)) as Function of (M2 | (h " U)), (M1 | U) by JORDAN24: 12;

      

       A7: (h " ( Int U)) c= (h " U) by TOPS_1: 16, RELAT_1: 143;

      hhU is being_homeomorphism by A3, A6, METRIZTS: 2;

      then

       A8: ((M2 | (h " U)),(M1 | U)) are_homeomorphic by T_0TOPSP:def 1;

      (h " ( Int U)) is open by A5, A3, TOPS_2: 43;

      then

       A9: (h " ( Int U)) c= ( Int (h " U)) by A7, TOPS_1: 24;

      

       A10: ( dom h) = ( [#] M2) by A3, TOPS_2:def 5;

      hp in ( Int U) by CONNSP_2:def 1;

      then p in (h " ( Int U)) by FUNCT_1:def 7, A10;

      then (h " U) is a_neighborhood of p by A9, CONNSP_2:def 1;

      hence thesis by A8, A4, BORSUK_3: 3;

    end;

    theorem :: MFOLD_0:11

    

     Th11: M1 is n -locally_euclidean & M2 is locally_euclidean & (M1,M2) are_homeomorphic implies M2 is n -locally_euclidean

    proof

      assume that

       A1: M1 is n -locally_euclidean and

       A2: M2 is locally_euclidean and

       A3: (M1,M2) are_homeomorphic ;

      consider h be Function of M1, M2 such that

       A4: h is being_homeomorphism by A3, T_0TOPSP:def 1;

      let q be Point of M2;

      set hp = q;

      consider W be a_neighborhood of hp, m such that

       A5: ((M2 | W),( Tdisk (( 0. ( TOP-REAL m)),1))) are_homeomorphic by A2;

      

       A6: ( rng h) = ( [#] M2) by A4, TOPS_2:def 5;

      then

       A7: (h " W) is non empty by RELAT_1: 139;

      

       A8: ( dom h) = ( [#] M1) by A4, TOPS_2:def 5;

      then

      consider p be object such that

       A9: p in ( [#] M1) and

       A10: (h . p) = q by A6, FUNCT_1:def 3;

      reconsider p as Point of M1 by A9;

      consider U be a_neighborhood of p such that

       A11: ((M1 | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A1;

      consider h2 be Function of (M2 | W), ( Tdisk (( 0. ( TOP-REAL m)),1)) such that

       A12: h2 is being_homeomorphism by T_0TOPSP:def 1, A5;

      

       A13: (h .: (h " W)) = W by A6, FUNCT_1: 77;

      then

      reconsider hhW = (h | (h " W)) as Function of (M1 | (h " W)), (M2 | W) by JORDAN24: 12;

      hhW is being_homeomorphism by A4, A13, METRIZTS: 2;

      then (h2 * hhW) is being_homeomorphism by A7, A12, TOPS_2: 57;

      then

       A14: ((M1 | (h " W)),( Tdisk (( 0. ( TOP-REAL m)),1))) are_homeomorphic by T_0TOPSP:def 1;

      

       A15: (h " ( Int W)) c= (h " W) by TOPS_1: 16, RELAT_1: 143;

      (h " ( Int W)) is open by A6, A4, TOPS_2: 43;

      then

       A16: (h " ( Int W)) c= ( Int (h " W)) by A15, TOPS_1: 24;

      hp in ( Int W) by CONNSP_2:def 1;

      then

       A17: p in (h " ( Int W)) by A10, FUNCT_1:def 7, A8;

      p in ( Int U) by CONNSP_2:def 1;

      then n = m by A17, A16, XBOOLE_0: 3, A14, A11, BROUWER3: 14;

      hence thesis by A5;

    end;

    ::$Notion-Name

    theorem :: MFOLD_0:12

    M is n -locally_euclidean & M is m -locally_euclidean implies n = m

    proof

      assume that

       A1: M is n -locally_euclidean and

       A2: M is m -locally_euclidean;

      set p = the Point of M;

      consider W be a_neighborhood of p such that

       A3: ((M | W),( Tdisk (( 0. ( TOP-REAL m)),1))) are_homeomorphic by A2;

      consider U be a_neighborhood of p such that

       A4: ((M | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A1;

      

       A5: p in ( Int W) by CONNSP_2:def 1;

      p in ( Int U) by CONNSP_2:def 1;

      hence thesis by A5, XBOOLE_0: 3, A4, A3, BROUWER3: 14;

    end;

    theorem :: MFOLD_0:13

    

     Th13: M is without_boundaryn -locally_euclidean non empty TopSpace iff for p be Point of M holds ex U be a_neighborhood of p st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic

    proof

      set TR = ( TOP-REAL n);

      hereby

        assume

         A1: M is without_boundaryn -locally_euclidean non empty TopSpace;

        then

        reconsider MM = M as without_boundaryn -locally_euclidean non empty TopSpace;

        let p be Point of M;

        consider U be a_neighborhood of p such that

         A2: ((M | U),( Tdisk (( 0. TR),1))) are_homeomorphic by Def3, A1;

        set MU = (M | U);

        consider h be Function of MU, ( Tdisk (( 0. TR),1)) such that

         A3: h is being_homeomorphism by A2, T_0TOPSP:def 1;

        

         A4: ( [#] ( Tdisk (( 0. TR),1))) = ( cl_Ball (( 0. TR),1)) by PRE_TOPC:def 5;

        then

        reconsider B = ( Ball (( 0. TR),1)) as Subset of ( Tdisk (( 0. TR),1)) by TOPREAL9: 16;

        reconsider B as open Subset of ( Tdisk (( 0. TR),1)) by TSEP_1: 9;

        

         A5: ( Int U) c= U by TOPS_1: 16;

        set HIB = (B /\ (h .: ( Int U)));

        reconsider hib = HIB as Subset of TR by A4, XBOOLE_1: 1;

        

         A6: HIB c= ( Ball (( 0. TR),1)) by XBOOLE_1: 17;

        

         A7: (h " HIB) c= (h " (h .: ( Int U))) by XBOOLE_1: 17, RELAT_1: 143;

        

         A8: (h " (h .: ( Int U))) c= ( Int U) by A3, FUNCT_1: 82;

        

         A9: ( cl_Ball (( 0. TR),1)) = (( Ball (( 0. TR),1)) \/ ( Sphere (( 0. TR),1))) by TOPREAL9: 18;

        

         A10: ( [#] MU) = U by PRE_TOPC:def 5;

        then

        reconsider IU = ( Int U) as Subset of (M | U) by TOPS_1: 16;

        

         A11: p in ( Int U) by CONNSP_2:def 1;

        

         A12: ( dom h) = ( [#] MU) by A3, TOPS_2:def 5;

        then

         A13: (h . p) in ( rng h) by A11, A5, A10, FUNCT_1:def 3;

        

         A14: (h . p) in ( Ball (( 0. TR),1))

        proof

          assume not (h . p) in ( Ball (( 0. TR),1));

          then (h . p) in ( Sphere (( 0. TR),1)) by A4, A13, A9, XBOOLE_0:def 3;

          then p in ( Fr MM) by A3, Th5;

          hence contradiction;

        end;

        then

        reconsider hP = (h . p) as Point of TR;

        IU is open by TSEP_1: 9;

        then (h .: ( Int U)) is open by A3, TOPGRP_1: 25;

        then

         A15: hib is open by TSEP_1: 9, A6;

        (h . p) in (h .: ( Int U)) by A11, A5, A10, A12, FUNCT_1:def 6;

        then (h . p) in hib by A14, XBOOLE_0:def 4;

        then

        consider r be positive Real such that

         A16: ( Ball (hP,r)) c= hib by A15, TOPS_4: 2;

         |.(hP - hP).| = 0 by TOPRNS_1: 28;

        then

         A17: hP in ( Ball (hP,r));

        reconsider bb = ( Ball (hP,r)) as non empty Subset of ( Tdisk (( 0. TR),1)) by A16, XBOOLE_1: 1;

        reconsider hb = (h " bb) as Subset of M by A10, XBOOLE_1: 1;

        bb is open by TSEP_1: 9;

        then

         A18: (h " bb) is open by A3, TOPGRP_1: 26;

        

         A19: (M | hb) = ((M | U) | (h " bb)) by A10, PRE_TOPC: 7;

        hb c= (h " HIB) by A16, RELAT_1: 143;

        then hb c= ( Int U) by A7, A8;

        then

         A20: hb is open by A10, TSEP_1: 9, A18, A5;

        p in hb by A17, A11, A5, A10, A12, FUNCT_1:def 7;

        then

         A21: p in ( Int hb) by A20, TOPS_1: 23;

        ( rng h) = ( [#] ( Tdisk (( 0. TR),1))) by A3, TOPS_2:def 5;

        then

         A22: (h .: (h " bb)) = bb by FUNCT_1: 77;

        

         A24: (( Tdisk (( 0. TR),1)) | bb) = (TR | ( Ball (hP,r))) by A4, PRE_TOPC: 7;

        then

        reconsider hh = (h | (h " bb)) as Function of (M | hb), ( Tball (hP,r)) by A19, JORDAN24: 12, A22;

        reconsider hb as a_neighborhood of p by A21, CONNSP_2:def 1;

        hh is being_homeomorphism by A3, A19, A22, A24, METRIZTS: 2;

        then

         A25: ((M | hb),( Tball (hP,r))) are_homeomorphic by T_0TOPSP:def 1;

        take hb;

        (( Tball (hP,r)),( Tball (( 0. TR),1))) are_homeomorphic by Th3;

        hence ((M | hb),( Tball (( 0. TR),1))) are_homeomorphic by A25, BORSUK_3: 3;

      end;

      assume

       A26: for p be Point of M holds ex U be a_neighborhood of p st ((M | U),( Tball (( 0. TR),1))) are_homeomorphic ;

      M is n -locally_euclidean

      proof

        ( [#] ( Tdisk (( 0. TR),1))) = ( cl_Ball (( 0. TR),1)) by PRE_TOPC:def 5;

        then

        reconsider B = ( Ball (( 0. TR),1)) as Subset of ( Tdisk (( 0. TR),1)) by TOPREAL9: 16;

        reconsider B as open Subset of ( Tdisk (( 0. TR),1)) by TSEP_1: 9;

        let p be Point of M;

        consider U be a_neighborhood of p such that

         A27: ((M | U),( Tball (( 0. TR),1))) are_homeomorphic by A26;

        

         A28: n in NAT by ORDINAL1:def 12;

        

         A30: ( [#] ( Tball (( 0. TR),1))) = ( Ball (( 0. TR),1)) by PRE_TOPC:def 5;

        then

        reconsider clB = ( cl_Ball (( 0. TR),(1 / 2))) as non empty Subset of ( Tball (( 0. TR),1)) by JORDAN: 21, A28;

        set MU = (M | U);

        consider h be Function of MU, ( Tball (( 0. TR),1)) such that

         A31: h is being_homeomorphism by A27, T_0TOPSP:def 1;

        set En = ( Euclid n);

        

         A32: ( Int U) c= U by TOPS_1: 16;

        

         A33: ( [#] MU) = U by PRE_TOPC:def 5;

        then

        reconsider IU = ( Int U) as Subset of (M | U) by TOPS_1: 16;

        reconsider hIU = (h .: IU) as Subset of TR by A30, XBOOLE_1: 1;

        

         A34: ( dom h) = ( [#] MU) by A31, TOPS_2:def 5;

        then

         A35: IU = (h " hIU) by A31, FUNCT_1: 82, FUNCT_1: 76;

        

         A36: the TopStruct of TR = ( TopSpaceMetr En) by EUCLID:def 8;

        then

        reconsider hIUE = hIU as Subset of ( TopSpaceMetr En);

        

         A37: p in ( Int U) by CONNSP_2:def 1;

        then

         A38: (h . p) in hIU by A34, FUNCT_1:def 6;

        then

        reconsider hp = (h . p) as Point of En by EUCLID: 67;

        reconsider Hp = (h . p) as Point of TR by A38;

        IU is open by TSEP_1: 9;

        then (h .: IU) is open by A31, TOPGRP_1: 25;

        then hIU is open by A30, TSEP_1: 9;

        then hIU in the topology of TR by PRE_TOPC:def 2;

        then

        consider r be Real such that

         A39: r > 0 and

         A40: ( Ball (hp,r)) c= hIUE by A38, A36, PRE_TOPC:def 2, TOPMETR: 15;

        set r2 = (r / 2);

        

         A41: ( Ball (Hp,r)) = ( Ball (hp,r)) by TOPREAL9: 13;

        ( cl_Ball (Hp,r2)) c= ( Ball (Hp,r)) by A28, XREAL_1: 216, A39, JORDAN: 21;

        then

         A42: ( cl_Ball (Hp,r2)) c= hIU by A40, A41;

        then

        reconsider CL = ( cl_Ball (Hp,r2)) as Subset of ( Tball (( 0. TR),1)) by XBOOLE_1: 1;

        

         A43: ( cl_Ball (Hp,r2)) c= ( [#] ( Tball (( 0. TR),1))) by A42, XBOOLE_1: 1;

        then ( cl_Ball (Hp,r2)) c= ( rng h) by A31, TOPS_2:def 5;

        then

         A44: (h .: (h " CL)) = CL by FUNCT_1: 77;

        set r22 = (r2 / 2);

        r22 < r2 by A39, XREAL_1: 216;

        then

         A45: ( Ball (Hp,r22)) c= ( Ball (Hp,r2)) by A28, JORDAN: 18;

        reconsider hCL = (h " CL) as Subset of M by A33, XBOOLE_1: 1;

        

         A46: ((M | U) | (h " CL)) = (M | hCL) by A33, PRE_TOPC: 7;

        

         A47: ( Ball (Hp,r2)) c= ( cl_Ball (Hp,r2)) by TOPREAL9: 16;

        then

         A48: ( Ball (Hp,r22)) c= ( cl_Ball (Hp,r2)) by A45;

        then

        reconsider BI = ( Ball (Hp,r22)) as Subset of ( Tball (( 0. TR),1)) by A43, XBOOLE_1: 1;

        BI c= hIU by A42, A47, A45;

        then

         A49: (h " BI) c= (h " hIU) by RELAT_1: 143;

        reconsider hBI = (h " BI) as Subset of M by A33, XBOOLE_1: 1;

        BI is open by TSEP_1: 9;

        then (h " BI) is open by A31, TOPGRP_1: 26;

        then

         A50: hBI is open by A35, A49, TSEP_1: 9;

         |.(Hp - Hp).| = 0 by TOPRNS_1: 28;

        then (h . p) in BI by A39;

        then p in (h " BI) by A37, A32, A33, A34, FUNCT_1:def 7;

        then p in ( Int hCL) by A48, RELAT_1: 143, TOPS_1: 22, A50;

        then

        reconsider hCL as a_neighborhood of p by CONNSP_2:def 1;

        

         A51: (( Tball (( 0. TR),1)) | CL) = ( Tdisk (Hp,r2)) by A30, PRE_TOPC: 7;

        then

        reconsider hh = (h | (h " CL)) as Function of (M | hCL), ( Tdisk (Hp,r2)) by A44, JORDAN24: 12, A46;

        hh is being_homeomorphism by A31, A51, METRIZTS: 2, A44, A46;

        then

         A52: ((M | hCL),( Tdisk (Hp,r2))) are_homeomorphic by T_0TOPSP:def 1;

        (( Tdisk (Hp,r2)),( Tdisk (( 0. TR),1))) are_homeomorphic by Lm1, A39;

        hence thesis by A52, BORSUK_3: 3, A39;

      end;

      then

      reconsider M as n -locally_euclidean non empty TopSpace;

      M is without_boundary

      proof

        thus ( Int M) c= the carrier of M;

        let x be object;

        assume x in the carrier of M;

        then

        reconsider p = x as Point of M;

        ex U be a_neighborhood of p st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A26;

        hence thesis by Def4;

      end;

      hence thesis;

    end;

    ::$Notion-Name

    registration

      let n,m be Element of NAT ;

      let N be n -locally_euclidean non empty TopSpace;

      let M be m -locally_euclidean non empty TopSpace;

      cluster [:N, M:] -> (n + m) -locally_euclidean;

      coherence

      proof

        reconsider nm = (n + m) as Nat;

        let p be Point of [:N, M:];

        ex hf be Function of [:( Tdisk (( 0. ( TOP-REAL n)),1)), ( Tdisk (( 0. ( TOP-REAL m)),1)):], ( Tdisk (( 0. ( TOP-REAL (n + m))),1)) st hf is being_homeomorphism & (hf .: [:( Ball (( 0. ( TOP-REAL n)),1)), ( Ball (( 0. ( TOP-REAL m)),1)):]) = ( Ball (( 0. ( TOP-REAL nm)),1)) by TIETZE_2: 19;

        then

         A1: ( [:( Tdisk (( 0. ( TOP-REAL n)),1)), ( Tdisk (( 0. ( TOP-REAL m)),1)):],( Tdisk (( 0. ( TOP-REAL nm)),1))) are_homeomorphic by T_0TOPSP:def 1;

        p in the carrier of [:N, M:];

        then p in [:the carrier of N, the carrier of M:] by BORSUK_1:def 2;

        then

        consider x,y be object such that

         A2: x in the carrier of N and

         A3: y in the carrier of M and

         A4: p = [x, y] by ZFMISC_1:def 2;

        reconsider x as Point of N by A2;

        consider Ux be a_neighborhood of x such that

         A5: ((N | Ux),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Def3;

        reconsider y as Point of M by A3;

        consider Uy be a_neighborhood of y such that

         A6: ((M | Uy),( Tdisk (( 0. ( TOP-REAL m)),1))) are_homeomorphic by Def3;

        consider hy be Function of (M | Uy), ( Tdisk (( 0. ( TOP-REAL m)),1)) such that

         A7: hy is being_homeomorphism by A6, T_0TOPSP:def 1;

        consider hx be Function of (N | Ux), ( Tdisk (( 0. ( TOP-REAL n)),1)) such that

         A8: hx is being_homeomorphism by A5, T_0TOPSP:def 1;

         [:hx, hy:] is being_homeomorphism by A7, TIETZE_2: 15, A8;

        then

         A9: ( [:(N | Ux), (M | Uy):], [:( Tdisk (( 0. ( TOP-REAL n)),1)), ( Tdisk (( 0. ( TOP-REAL m)),1)):]) are_homeomorphic by T_0TOPSP:def 1;

         [:(N | Ux), (M | Uy):] = ( [:N, M:] | [:Ux, Uy:]) by BORSUK_3: 22;

        hence thesis by A1, A9, BORSUK_3: 3, A4;

      end;

    end

    ::$Notion-Name

    registration

      let n;

      let M be n -locally_euclidean non empty TopSpace;

      cluster (M | ( Int M)) -> n -locally_euclidean;

      coherence

      proof

        set MI = (M | ( Int M));

        

         A1: ( [#] MI) = ( Int M) by PRE_TOPC:def 5;

        for p be Point of MI holds ex U be a_neighborhood of p st ((MI | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic

        proof

          let p be Point of MI;

          p in ( Int M) by A1;

          then

          reconsider q = p as Point of M;

          consider U be a_neighborhood of q such that

           A2: ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A1, Def7;

          set MU = (M | U), TR = ( TOP-REAL n);

          consider h be Function of MU, ( Tball (( 0. TR),1)) such that

           A3: h is being_homeomorphism by A2, T_0TOPSP:def 1;

          

           A4: ( Int U) c= U by TOPS_1: 16;

          

           A5: (( Int M) /\ ( Int U)) in the topology of M by PRE_TOPC:def 2;

          

           A6: ( Int U) c= U by TOPS_1: 16;

          

           A7: ( [#] MU) = U by PRE_TOPC:def 5;

          (( Int U) /\ ( Int M)) c= ( Int U) by XBOOLE_1: 17;

          then

          reconsider UIM = (( Int M) /\ ( Int U)) as Subset of MU by A6, A7, XBOOLE_1: 1;

          

           A8: (h " (h .: UIM)) c= UIM by A3, FUNCT_1: 82;

          

           A9: ( dom h) = ( [#] MU) by A3, TOPS_2:def 5;

          

           A11: ( [#] ( Tball (( 0. TR),1))) = ( Ball (( 0. TR),1)) by PRE_TOPC:def 5;

          then

          reconsider hum = (h .: UIM) as Subset of TR by XBOOLE_1: 1;

          (UIM /\ ( [#] MU)) = UIM by XBOOLE_1: 28;

          then UIM in the topology of MU by A5, PRE_TOPC:def 4;

          then UIM is open by PRE_TOPC:def 2;

          then (h .: UIM) is open by A3, TOPGRP_1: 25;

          then hum is open by TSEP_1: 9, A11;

          then

           A12: ( Int hum) = hum by TOPS_1: 23;

          

           A13: q in ( Int U) by CONNSP_2:def 1;

          then

           A14: q in UIM by A1, XBOOLE_0:def 4;

          then (h . q) in hum by A9, FUNCT_1:def 6;

          then

          reconsider hq = (h . q) as Point of TR;

          reconsider HQ = hq as Point of ( Euclid n) by EUCLID: 67;

          (h . q) in (h .: UIM) by A14, A9, FUNCT_1:def 6;

          then

          consider s be Real such that

           A15: s > 0 and

           A16: ( Ball (HQ,s)) c= hum by A12, GOBOARD6: 5;

          

           A17: ( Ball (HQ,s)) = ( Ball (hq,s)) by TOPREAL9: 13;

          then

          reconsider BB = ( Ball (hq,s)) as Subset of ( Tball (( 0. TR),1)) by A16, XBOOLE_1: 1;

          BB is open by TSEP_1: 9;

          then

          reconsider hBB = (h " BB) as open Subset of MU by A3, TOPGRP_1: 26;

          hBB c= (h " (h .: UIM)) by A16, A17, RELAT_1: 143;

          then

           A18: hBB c= UIM by A8;

          reconsider hBBM = hBB as Subset of M by A7, XBOOLE_1: 1;

          (( Int U) /\ ( Int M)) c= ( Int M) by XBOOLE_1: 17;

          then

          reconsider HBB = hBBM as Subset of MI by A18, XBOOLE_1: 1, A1;

          hBBM is open by TSEP_1: 9, A18;

          then

           A19: HBB is open by TSEP_1: 9;

           |.(hq - hq).| = 0 by TOPRNS_1: 28;

          then hq in BB by A15;

          then p in HBB by FUNCT_1:def 7, A13, A4, A9, A7;

          then

           A20: p in ( Int HBB) by A19, TOPS_1: 23;

          

           A21: (M | hBBM) = (MI | HBB) by A1, PRE_TOPC: 7;

          ( rng h) = ( [#] ( Tball (( 0. TR),1))) by A3, TOPS_2:def 5;

          then (h .: hBB) = BB by FUNCT_1: 77;

          then

           A22: (( Tball (( 0. TR),1)) | (h .: hBB)) = (TR | ( Ball (hq,s))) by A11, PRE_TOPC: 7;

          reconsider HBB as a_neighborhood of p by A20, CONNSP_2:def 1;

          

           A23: (MU | hBB) = (M | hBBM) by A7, PRE_TOPC: 7;

          then

          reconsider hh = (h | hBB) as Function of (MI | HBB), (TR | ( Ball (hq,s))) by A22, JORDAN24: 12, A21;

          hh is being_homeomorphism by A3, A22, A23, A21, METRIZTS: 2;

          then

           A24: ((MI | HBB),( Tball (hq,s))) are_homeomorphic by T_0TOPSP:def 1;

          take HBB;

          (( Tball (hq,s)),( Tball (( 0. TR),1))) are_homeomorphic by A15, Th3;

          hence thesis by A15, A24, BORSUK_3: 3;

        end;

        hence thesis by Th13;

      end;

    end

    ::$Notion-Name

    registration

      let n be non zero Nat;

      let M be with_boundaryn -locally_euclidean non empty TopSpace;

      cluster (M | ( Fr M)) -> (n -' 1) -locally_euclidean;

      coherence

      proof

        set MF = (M | ( Fr M));

        n > 0 ;

        then

        reconsider n1 = (n - 1) as Nat by NAT_1: 20;

        

         A1: ( [#] MF) = ( Fr M) by PRE_TOPC:def 5;

         A2:

        now

          let pF be Point of MF;

          pF in ( [#] MF);

          then

          reconsider p = pF as Point of M by A1;

          consider U be a_neighborhood of p such that

           A3: ((M | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Def3;

          ((M | U),( Tdisk (( 0. ( TOP-REAL (n1 + 1))),1))) are_homeomorphic by A3;

          hence ex W be a_neighborhood of pF st ((MF | W),( Tball (( 0. ( TOP-REAL n1)),1))) are_homeomorphic by Th7;

        end;

        (n -' 1) = n1 by XREAL_0:def 2;

        hence thesis by A2, Th13;

      end;

    end

    begin

    theorem :: MFOLD_0:14

    

     Th14: for M be compact locally_euclidean non empty TopSpace holds for C be Subset of M st C is a_component holds C is open & ex n st (M | C) is n -locally_euclidean non empty TopSpace

    proof

      let M be compact locally_euclidean non empty TopSpace;

      defpred P[ Point of M, Subset of M] means $2 is a_neighborhood of $1 & ex n st ((M | $2),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

      let C be Subset of M such that

       A1: C is a_component;

      consider p be object such that

       A2: p in C by A1, XBOOLE_0:def 1;

      reconsider p as Point of M by A2;

      

       A3: for x be Point of M holds ex y be Element of ( bool the carrier of M) st P[x, y]

      proof

        let x be Point of M;

        ex U be a_neighborhood of x, n st ((M | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by Def2;

        hence thesis;

      end;

      consider W be Function of M, ( bool the carrier of M) such that

       A4: for x be Point of M holds P[x, (W . x)] from FUNCT_2:sch 3( A3);

      reconsider MC = (M | C) as non empty connected TopSpace by A1, CONNSP_1:def 3;

      defpred CC[ object, object] means $2 in C & for A be Subset of M st A = (W . $2) holds ( Int A) = $1;

      set IntW = { ( Int U) where U be Subset of M : U in ( rng (W | C)) };

      IntW c= ( bool the carrier of M)

      proof

        let x be object;

        assume x in IntW;

        then ex U be Subset of M st x = ( Int U) & U in ( rng (W | C));

        hence thesis;

      end;

      then

      reconsider IntW as Subset-Family of M;

      reconsider R = (IntW \/ {(C ` )}) as Subset-Family of M;

      for A be Subset of M st A in R holds A is open

      proof

        let A be Subset of M such that

         A5: A in R;

        per cases by ZFMISC_1: 136, A5;

          suppose A = (C ` );

          hence thesis by A1;

        end;

          suppose A in IntW;

          then ex U be Subset of M st A = ( Int U) & U in ( rng (W | C));

          hence thesis;

        end;

      end;

      then

       A6: R is open by TOPS_2:def 1;

      

       A7: for A be Subset of M st A in ( rng W) holds A is connected & ( Int A) is non empty

      proof

        let A be Subset of M;

        assume A in ( rng W);

        then

        consider p be object such that

         A8: p in ( dom W) and

         A9: (W . p) = A by FUNCT_1:def 3;

        consider n such that

         A10: ((M | A),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A8, A9, A4;

        reconsider AA = A as non empty Subset of M by A8, A9, A4;

        

         A11: ( Tdisk (( 0. ( TOP-REAL n)),1)) is connected by CONNSP_1:def 3;

        (( Tdisk (( 0. ( TOP-REAL n)),1)),(M | AA)) are_homeomorphic by A10;

        then

        consider h be Function of ( Tdisk (( 0. ( TOP-REAL n)),1)), (M | A) such that

         A12: h is being_homeomorphism by T_0TOPSP:def 1;

        reconsider p as Point of M by A8;

        

         A13: P[p, A] by A8, A9, A4;

        

         A14: ( rng h) = ( [#] (M | A)) by A12, TOPS_2:def 5;

        

         A15: (h .: ( dom h)) = ( rng h) by RELAT_1: 113;

        ( dom h) = ( [#] ( Tdisk (( 0. ( TOP-REAL n)),1))) by A12, TOPS_2:def 5;

        then (M | A) is connected by A15, A14, A12, A11, CONNSP_1: 14;

        hence thesis by CONNSP_1:def 3, A13, CONNSP_2:def 1;

      end;

      

       A16: ( dom W) = the carrier of M by FUNCT_2:def 1;

      the carrier of M c= ( union R)

      proof

        let x be object;

        assume x in the carrier of M;

        then

        reconsider x as Point of M;

        per cases ;

          suppose x in C;

          then

           A17: x in ( dom (W | C)) by RELAT_1: 57, A16;

          then

           A18: ((W | C) . x) = (W . x) by FUNCT_1: 47;

          ((W | C) . x) in ( rng (W | C)) by A17, FUNCT_1:def 3;

          then ( Int (W . x)) in IntW by A18;

          then

           A19: ( Int (W . x)) in R by XBOOLE_0:def 3;

          (W . x) is a_neighborhood of x by A4;

          then x in ( Int (W . x)) by CONNSP_2:def 1;

          hence thesis by A19, TARSKI:def 4;

        end;

          suppose not x in C;

          then x in (( [#] M) \ C) by XBOOLE_0:def 5;

          then

           A20: x in (C ` ) by SUBSET_1:def 4;

          (C ` ) in R by ZFMISC_1: 136;

          hence thesis by A20, TARSKI:def 4;

        end;

      end;

      then

      consider R1 be Subset-Family of M such that

       A21: R1 c= R and

       A22: R1 is Cover of M and

       A23: R1 is finite by SETFAM_1:def 11, A6, COMPTS_1:def 1;

      reconsider R1 as finite Subset-Family of M by A23;

      set R2 = (R1 \ {(C ` )});

      ( union R1) = the carrier of M by A22, SETFAM_1: 45;

      

      then

       A24: (( union R1) \ ( union {(C ` )})) = (the carrier of M \ (C ` )) by ZFMISC_1: 25

      .= ((C ` ) ` ) by SUBSET_1:def 4

      .= C;

      then C c= ( union R2) by TOPS_2: 4;

      then

      consider xp be set such that p in xp and

       A25: xp in R2 by A2, TARSKI:def 4;

      

       A26: C = ( Component_of C) by A1, CONNSP_3: 7;

      for x be set holds x in C iff ex Q be Subset of M st Q is open & Q c= C & x in Q

      proof

        let x be set;

        hereby

          assume

           A27: x in C;

          then

          reconsider p = x as Point of M;

          take I = ( Int (W . p));

          

           A28: ( Int (W . p)) c= (W . p) by TOPS_1: 16;

          (W . p) in ( rng W) by A16, FUNCT_1:def 3;

          then

           A29: (W . p) is connected by A7;

          

           A30: (W . p) is a_neighborhood of p by A4;

          then p in ( Int (W . p)) by CONNSP_2:def 1;

          then (W . p) meets C by A28, A27, XBOOLE_0: 3;

          then (W . p) c= C by A1, A29, CONNSP_3: 16, A26;

          hence I is open & I c= C & x in I by A30, CONNSP_2:def 1, A28;

        end;

        thus thesis;

      end;

      hence C is open by TOPS_1: 25;

      

       A31: R2 c= R1 by XBOOLE_1: 36;

      

       A32: ( rng (W | C)) c= ( rng W) by RELAT_1: 70;

      ( union R2) c= C

      proof

        let x be object;

        assume x in ( union R2);

        then

        consider y be set such that

         A33: x in y and

         A34: y in R2 by TARSKI:def 4;

        y in R1 by A34, ZFMISC_1: 56;

        then y in IntW or y = (C ` ) by A21, ZFMISC_1: 136;

        then

        consider U be Subset of M such that

         A35: y = ( Int U) and

         A36: U in ( rng (W | C)) by A34, ZFMISC_1: 56;

        

         A37: U is connected by A32, A36, A7;

        

         A38: ( Int U) c= U by TOPS_1: 16;

        consider p be object such that

         A39: p in ( dom (W | C)) and

         A40: ((W | C) . p) = U by A36, FUNCT_1:def 3;

        

         A41: (W . p) = U by A39, A40, FUNCT_1: 47;

        p in ( dom W) by A39, RELAT_1: 57;

        then

        reconsider p as Point of M;

        U is a_neighborhood of p by A4, A41;

        then p in ( Int U) by CONNSP_2:def 1;

        then (W . p) meets C by A38, A39, A41, XBOOLE_0: 3;

        then U c= C by A41, A1, A37, CONNSP_3: 16, A26;

        hence thesis by A38, A33, A35;

      end;

      then

       A42: ( union R2) = C by A24, TOPS_2: 4;

      

       A43: for x be object st x in R2 holds ex y be object st CC[x, y]

      proof

        let x be object;

        assume

         A44: x in R2;

        then

         A45: x <> (C ` ) by ZFMISC_1: 56;

        x in R1 by A44, ZFMISC_1: 56;

        then x in IntW by A21, A45, ZFMISC_1: 136;

        then

        consider U be Subset of M such that

         A46: x = ( Int U) and

         A47: U in ( rng (W | C));

        consider y be object such that

         A48: y in ( dom (W | C)) and

         A49: ((W | C) . y) = U by A47, FUNCT_1:def 3;

        take y;

        thus y in C by A48;

        let A be Subset of M;

        thus thesis by A48, FUNCT_1: 47, A46, A49;

      end;

      consider cc be Function such that

       A50: ( dom cc) = R2 & for x be object st x in R2 holds CC[x, (cc . x)] from CLASSES1:sch 1( A43);

       CC[xp, (cc . xp)] by A25, A50;

      then

      reconsider cp = (cc . xp) as Point of M;

      consider n such that

       A51: ((M | (W . cp)),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A4;

      defpred P[ Nat] means $1 <= ( card R2) implies ex R3 be Subset-Family of M st ( card R3) = $1 & R3 c= R2 & ( union (W .: (cc .: R3))) is connected Subset of M & for A,B be Subset of M st A in R3 & B = (W . (cc . A)) holds ((M | B),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

      

       A52: ( Int (W . cp)) = xp by A25, A50;

      

       A53: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A54: P[k];

        assume

         A55: (k + 1) <= ( card R2);

        then

        consider R3 be Subset-Family of M such that

         A56: ( card R3) = k and

         A57: R3 c= R2 and

         A58: ( union (W .: (cc .: R3))) is connected Subset of M and

         A59: for A,B be Subset of M st A in R3 & B = (W . (cc . A)) holds ((M | B),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by NAT_1: 13, A54;

        k < ( card R2) by A55, NAT_1: 13;

        then k in ( Segm ( card R2)) by NAT_1: 44;

        then (R2 \ R3) <> {} by A56, CARD_1: 68;

        then

        consider r23 be object such that

         A60: r23 in (R2 \ R3) by XBOOLE_0:def 1;

        reconsider r23 as set by TARSKI: 1;

        

         A61: r23 in R2 by A60, XBOOLE_0:def 5;

        then

         A62: r23 <> (C ` ) by ZFMISC_1: 56;

        r23 in R1 by A61, ZFMISC_1: 56;

        then r23 in IntW by A21, A62, ZFMISC_1: 136;

        then

         A63: ex B be Subset of M st ( Int B) = r23 & B in ( rng (W | C));

        

         A64: r23 c= ( union (R2 \ R3)) by A60, ZFMISC_1: 74;

        per cases ;

          suppose k > 0 ;

          then R3 is non empty by A56;

          then

          consider r3 be set such that

           A65: r3 in R3;

          

           A66: r3 <> (C ` ) by A57, A65, ZFMISC_1: 56;

          r3 in R1 by A57, A65, ZFMISC_1: 56;

          then r3 in IntW by A21, A66, ZFMISC_1: 136;

          then

           A67: ex A be Subset of M st ( Int A) = r3 & A in ( rng (W | C));

          r3 c= ( union R3) by A65, ZFMISC_1: 74;

          then

          reconsider U3 = ( union R3) as non empty Subset of M by A32, A67, A7;

          set A1 = the Subset of M;

          reconsider U23 = ( union (R2 \ R3)) as Subset of M;

          set D2 = ( Down (U3,C)), D23 = ( Down (U23,C));

          D2 = (U3 /\ C) by CONNSP_3:def 5;

          then

           A68: D2 = U3 by XBOOLE_1: 28, A42, A57, ZFMISC_1: 77;

          ((R2 \ R3) \/ R3) = (R2 \/ R3) by XBOOLE_1: 39

          .= R2 by A57, XBOOLE_1: 12;

          then (U3 \/ U23) = C by A42, ZFMISC_1: 78;

          then

           A69: (U3 \/ U23) = ( [#] MC) by PRE_TOPC:def 5;

          R3 c= R1 by A31, A57;

          then R3 is open by A21, XBOOLE_1: 1, A6, TOPS_2: 11;

          then

           A70: D2 is open by TOPS_2: 19, CONNSP_3: 28;

          

           A71: (R2 \ R3) c= R2 by XBOOLE_1: 36;

          then (R2 \ R3) c= R1 by A31;

          then (R2 \ R3) is open by A21, XBOOLE_1: 1, A6, TOPS_2: 11;

          then

           A72: D23 is open by TOPS_2: 19, CONNSP_3: 28;

          D23 = (U23 /\ C) by CONNSP_3:def 5;

          then

           A73: D23 = U23 by XBOOLE_1: 28, A71, A42, ZFMISC_1: 77;

          U23 <> ( {} MC) by A64, A32, A63, A7;

          then

          consider m be object such that

           A74: m in U3 and

           A75: m in U23 by A70, A72, A68, A73, A69, CONNSP_1: 11, XBOOLE_0: 3;

          consider m1 be set such that

           A76: m in m1 and

           A77: m1 in R3 by A74, TARSKI:def 4;

           CC[m1, (cc . m1)] by A57, A77, A50;

          then

          reconsider c1 = (cc . m1) as Point of M;

          consider m2 be set such that

           A78: m in m2 and

           A79: m2 in (R2 \ R3) by A75, TARSKI:def 4;

          

           A80: m2 in R2 by A79, XBOOLE_0:def 5;

          then CC[m2, (cc . m2)] by A50;

          then

          reconsider c2 = (cc . m2) as Point of M;

          set R4 = (R3 \/ {( Int (W . c2))});

          R3 is finite by A56;

          then

          reconsider R4 as finite Subset-Family of M;

          take R4;

          

           A81: ( Int (W . c2)) = m2 by A80, A50;

          then not ( Int (W . c2)) in R3 by A79, XBOOLE_0:def 5;

          hence ( card R4) = (k + 1) by A56, A57, CARD_2: 41;

          

           A82: m2 in R2 by A79, XBOOLE_0:def 5;

          then {m2} c= R2 by ZFMISC_1: 31;

          hence

           A83: R4 c= R2 by A81, A57, XBOOLE_1: 8;

          

           A84: (W . c2) in ( rng W) by A16, FUNCT_1:def 3;

          

           A85: ( Int (W . c1)) = m1 by A57, A77, A50;

          thus ( union (W .: (cc .: R4))) is connected Subset of M

          proof

            reconsider UWR3 = ( union (W .: (cc .: R3))) as connected Subset of M by A58;

            

             A86: ( Int (W . c2)) c= (W . c2) by TOPS_1: 16;

            c1 in (cc .: R3) by A77, A57, A50, FUNCT_1:def 6;

            then

             A87: (W . c1) in (W .: (cc .: R3)) by A16, FUNCT_1:def 6;

            ( Int (W . c1)) c= (W . c1) by TOPS_1: 16;

            then

             A88: m in UWR3 by A87, A85, A76, TARSKI:def 4;

            UWR3 c= ( Cl UWR3) by PRE_TOPC: 18;

            then ( Cl UWR3) meets (W . c2) by A86, A81, A78, A88, XBOOLE_0: 3;

            then

             A89: not (UWR3,(W . c2)) are_separated by CONNSP_1:def 1;

            (cc .: R4) = ((cc .: R3) \/ (cc .: {m2})) by A81, RELAT_1: 120

            .= ((cc .: R3) \/ ( Im (cc,m2))) by RELAT_1:def 16

            .= ((cc .: R3) \/ {(cc . m2)}) by FUNCT_1: 59, A82, A50;

            

            then (W .: (cc .: R4)) = ((W .: (cc .: R3)) \/ (W .: {c2})) by RELAT_1: 120

            .= ((W .: (cc .: R3)) \/ ( Im (W,c2))) by RELAT_1:def 16

            .= ((W .: (cc .: R3)) \/ {(W . c2)}) by A16, FUNCT_1: 59;

            

            then

             A90: ( union (W .: (cc .: R4))) = (UWR3 \/ ( union {(W . c2)})) by ZFMISC_1: 78

            .= (UWR3 \/ (W . c2)) by ZFMISC_1: 25;

            (W . c2) is connected by A84, A7;

            hence thesis by A89, CONNSP_1: 17, A90;

          end;

          let a,b be Subset of M such that

           A91: a in R4 and

           A92: b = (W . (cc . a));

          per cases by A91, ZFMISC_1: 136;

            suppose a in R3;

            hence thesis by A92, A59;

          end;

            suppose a = ( Int (W . c2));

            then ( Int b) = ( Int (W . c2)) by A80, A50, A92;

            then

             A93: m in ( Int b) by A80, A50, A78;

             CC[a, (cc . a)] by A91, A83, A50;

            then

            reconsider ca = (cc . a) as Point of M;

            

             A94: ((M | (W . c1)),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A77, A59;

             P[ca, (W . ca)] by A4;

            then

            consider mm be Nat such that

             A95: ((M | b),( Tdisk (( 0. ( TOP-REAL mm)),1))) are_homeomorphic by A92;

            ( Int (W . c1)) = m1 by A57, A77, A50;

            then n = mm by A94, A76, A93, XBOOLE_0: 3, A95, BROUWER3: 14;

            hence ((M | b),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A95;

          end;

        end;

          suppose

           A96: k = 0 ;

          reconsider R3 = {( Int (W . cp))} as Subset-Family of M;

          take R3;

          thus ( card R3) = (k + 1) by A96, CARD_1: 30;

          thus

           A97: R3 c= R2 by A52, A25, ZFMISC_1: 31;

          (cc .: R3) = ( Im (cc,xp)) by A52, RELAT_1:def 16

          .= {cp} by FUNCT_1: 59, A25, A50;

          

          then (W .: (cc .: R3)) = ( Im (W,cp)) by RELAT_1:def 16

          .= {(W . cp)} by A16, FUNCT_1: 59;

          then

           A98: ( union (W .: (cc .: R3))) = (W . cp) by ZFMISC_1: 25;

          (W . cp) in ( rng W) by A16, FUNCT_1:def 3;

          hence ( union (W .: (cc .: R3))) is connected Subset of M by A98, A7;

          let a,b be Subset of M such that

           A99: a in R3 and

           A100: b = (W . (cc . a));

           CC[a, (cc . a)] by A99, A97, A50;

          then

          reconsider ca = (cc . a) as Point of M;

          ( Int (W . cp)) = xp by A25, A50;

          hence ((M | b),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A51, TARSKI:def 1, A99, A100;

        end;

      end;

      take n;

      

       A101: P[ 0 ]

      proof

        set R3 = the empty Subset of ( bool the carrier of M);

        assume 0 <= ( card R2);

        take R3;

        thus ( card R3) = 0 & R3 c= R2;

        reconsider UR3 = ( union (W .: (cc .: R3))) as empty Subset of M by ZFMISC_1: 2;

        UR3 is connected;

        hence ( union (W .: (cc .: R3))) is connected Subset of M;

        let A,B be Subset of M;

        thus thesis;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A101, A53);

      then P[( card R2)];

      then

      consider R3 be Subset-Family of M such that

       A102: ( card R3) = ( card R2) and

       A103: R3 c= R2 and

       A104: for A,B be Subset of M st A in R3 & B = (W . (cc . A)) holds ((M | B),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

      

       A105: R2 = R3 by A102, A103, CARD_2: 102;

      for p be Point of MC holds ex U be a_neighborhood of p st ((MC | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic

      proof

        let q be Point of MC;

        

         A106: ( [#] MC) = C by PRE_TOPC:def 5;

        then

        consider y be set such that

         A107: q in y and

         A108: y in R2 by A42, TARSKI:def 4;

         CC[y, (cc . y)] by A50, A108;

        then

        reconsider c = (cc . y) as Point of M;

        reconsider Wc = (W . c) as Subset of M;

        

         A109: ( Int Wc) c= Wc by TOPS_1: 16;

        set D = ( Down (Wc,C)), DI = ( Down (( Int Wc),C));

        Wc in ( rng W) by A16, FUNCT_1:def 3;

        then

         A110: Wc is connected by A7;

        

         A111: ( Int Wc) = y by A50, A108;

        then Wc meets C by A109, A107, A106, XBOOLE_0: 3;

        then

         A112: Wc c= C by A110, A1, CONNSP_3: 16, A26;

        then ((W . c) /\ C) = (W . c) by XBOOLE_1: 28;

        then

         A113: D = (W . c) by CONNSP_3:def 5;

        (( Int Wc) /\ C) = ( Int Wc) by A112, A109, XBOOLE_1: 1, XBOOLE_1: 28;

        then DI = ( Int Wc) by CONNSP_3:def 5;

        then q in ( Int D) by CONNSP_3: 28, A107, A111, A113, A109, TOPS_1: 22;

        then

         A114: D is a_neighborhood of q by CONNSP_2:def 1;

        (M | (W . c)) = ((M | C) | D) by A113, A106, PRE_TOPC: 7;

        hence thesis by A114, A104, A105, A108;

      end;

      hence thesis by Def3;

    end;

    theorem :: MFOLD_0:15

    for M be compact locally_euclidean non empty TopSpace holds ex P be a_partition of the carrier of M st for A be Subset of M st A in P holds A is open a_component & ex n st (M | A) is n -locally_euclidean non empty TopSpace

    proof

      let M be compact locally_euclidean non empty TopSpace;

      set P = { ( Component_of p) where p be Point of M : not contradiction };

      P c= ( bool the carrier of M)

      proof

        let x be object;

        assume x in P;

        then ex p be Point of M st x = ( Component_of p) & not contradiction;

        hence thesis;

      end;

      then

      reconsider P as Subset-Family of M;

      

       A1: the carrier of M c= ( union P)

      proof

        let x be object;

        assume x in the carrier of M;

        then

        reconsider x as Point of M;

        

         A2: ( Component_of x) in P;

        x in ( Component_of x) by CONNSP_1: 38;

        hence thesis by A2, TARSKI:def 4;

      end;

      for A be Subset of M st A in P holds A <> {} & for B be Subset of M st B in P holds A = B or A misses B

      proof

        let A be Subset of M;

        assume A in P;

        then

        consider p be Point of M such that

         A3: A = ( Component_of p) and not contradiction;

        thus A <> {} by A3;

        let B be Subset of M such that

         A4: B in P and

         A5: B <> A;

        

         A6: ex q be Point of M st B = ( Component_of q) & not contradiction by A4;

        assume A meets B;

        then

        consider x be object such that

         A7: x in A and

         A8: x in B by XBOOLE_0: 3;

        reconsider x as Point of M by A7;

        ( Component_of p) = ( Component_of x) by CONNSP_1: 42, A7, A3;

        hence thesis by CONNSP_1: 42, A8, A6, A5, A3;

      end;

      then

      reconsider P as a_partition of the carrier of M by A1, XBOOLE_0:def 10, EQREL_1:def 4;

      take P;

      let A be Subset of M;

      assume A in P;

      then ex p be Point of M st A = ( Component_of p) & not contradiction;

      then A is a_component by CONNSP_1: 40;

      hence thesis by Th14;

    end;

    theorem :: MFOLD_0:16

    for M be compact locally_euclidean non empty TopSpace st M is connected holds ex n st M is n -locally_euclidean

    proof

      let M be compact locally_euclidean non empty TopSpace;

      

       A1: for A be Subset of M st A is connected & ( [#] M) c= A holds A = ( [#] M);

      assume M is connected;

      then ( [#] M) is a_component by A1, CONNSP_1: 27, CONNSP_1:def 5;

      then

      consider n such that

       A2: (M | ( [#] M)) is n -locally_euclidean non empty TopSpace by Th14;

      ((M | ( [#] M)),M) are_homeomorphic by Th1;

      then M is n -locally_euclidean by Th11, A2;

      hence thesis;

    end;

    begin

    registration

      let n;

      cluster second-countable Hausdorffn -locally_euclidean for non empty TopSpace;

      existence

      proof

        take T = ( Tdisk (( 0. ( TOP-REAL n)),1));

        thus thesis;

      end;

    end

    definition

      mode topological_manifold is second-countable Hausdorff locally_euclidean non empty TopSpace;

    end

    notation

      let n;

      let M be topological_manifold;

      synonym M is n -dimensional for M is n -locally_euclidean;

    end

    registration

      let n;

      cluster n -dimensional without_boundary for topological_manifold;

      existence

      proof

        reconsider T = ( Tball (( 0. ( TOP-REAL n)),1)) as topological_manifold;

        T is without_boundary;

        hence thesis;

      end;

    end

    registration

      let n be non zero Nat;

      cluster n -dimensional compact with_boundary for topological_manifold;

      existence

      proof

        reconsider T = ( Tdisk (( 0. ( TOP-REAL n)),1)) as topological_manifold;

        T is compact;

        hence thesis;

      end;

    end

    registration

      let M be topological_manifold;

      cluster -> second-countable Hausdorff for non empty SubSpace of M;

      coherence

      proof

        let S be non empty SubSpace of M;

        ( [#] S) c= ( [#] M) by PRE_TOPC:def 4;

        then

        reconsider CS = ( [#] S) as Subset of M;

        consider B be Basis of (M | CS) such that

         A1: ( card B) = ( weight (M | CS)) by WAYBEL23: 74;

        

         A2: ( weight (M | CS)) c= omega by WAYBEL23:def 6;

        

         A3: the TopStruct of S = (S | ( [#] S)) by TSEP_1: 93;

        

         A4: (S | ( [#] S)) is SubSpace of M by TSEP_1: 7;

        ( [#] (S | ( [#] S))) = ( [#] S) by PRE_TOPC:def 5;

        then the TopStruct of S = (M | CS) by A3, A4, PRE_TOPC:def 5;

        then B is Basis of S by YELLOW12: 32;

        then ( weight S) c= ( card B) by WAYBEL23: 73;

        then ( weight S) c= omega by A1, A2;

        hence thesis;

      end;

    end

    registration

      let M1,M2 be topological_manifold;

      cluster [:M1, M2:] -> second-countable Hausdorff;

      coherence ;

    end