:: Topological Manifolds
::  by Karol P\kak
::
:: Received June 16, 2014
:: Copyright (c) 2014-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ARYTM_1, ARYTM_3, BROUWER, CARD_1, COMPLEX1, EUCLID, FUNCT_1,
      METRIC_1, NAT_1, NUMBERS, ORDINAL1, PCOMPS_1, PRE_TOPC, RCOMP_1, RELAT_1,
      STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TOPS_1, TOPS_2, XBOOLE_0, XREAL_0,
      XXREAL_0, XCMPLX_0, FINSET_1, ZFMISC_1, REAL_1, SETFAM_1, T_0TOPSP,
      CONNSP_2, MFOLD_1, RELAT_2, EQREL_1, CONNSP_1, CONNSP_3, MFOLD_0,
      WAYBEL23, COMPTS_1, RLVECT_3,ORDINAL2;
 notations TARSKI, XBOOLE_0, FINSET_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, COMPLEX1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0,
      XXREAL_3, NAT_1, CARD_1, REAL_1, SETFAM_1, STRUCT_0, PRE_TOPC, TOPS_1,
      METRIC_1, PCOMPS_1, RLVECT_1, EUCLID, TOPREAL9, TOPS_2, CONNSP_1,
      CONNSP_2, CONNSP_3, COMPTS_1, BROUWER, DOMAIN_1, ZFMISC_1,
      BORSUK_1, BORSUK_2, NAT_D, BINOP_1, EQREL_1, BORSUK_3, WAYBEL23,
      CANTOR_1, METRIZTS;
 constructors MONOID_0, CONVEX1, TOPREAL9, TOPS_1, COMPTS_1, FUNCSDOM, BROUWER,
      SEQ_4, EUCLID_9, SIMPLEX0, CONNSP_1, CONNSP_3, BORSUK_3, NAT_D,
      BORSUK_2, WAYBEL23, CANTOR_1, REAL_1,METRIZTS;
 registrations BORSUK_1, BROUWER, EUCLID, FUNCT_1, FUNCT_2, NAT_1, PRE_TOPC,
      RELAT_1, SIMPLEX2, STRUCT_0, SUBSET_1, TOPGRP_1, TOPS_1, XBOOLE_0,
      XREAL_0, XXREAL_0, RELSET_1, FINSET_1, TOPREALC, CARD_1, TOPREAL9,
      XXREAL_3, BORSUK_3, WAYBEL_2, XCMPLX_0, JORDAN1, BORSUK_2,
      CONNSP_1, ORDINAL1, METRIZTS, COMPTS_1, TOPREAL1;
 requirements ARITHM, BOOLE, NUMERALS, SUBSET, REAL;
 definitions TARSKI, XBOOLE_0;
 equalities BINOP_1, STRUCT_0, XCMPLX_0, TOPREAL9, BROUWER, ORDINAL1;
 expansions TARSKI, XBOOLE_0,WAYBEL23;
 theorems ABSVALUE, BORSUK_1, BROUWER, COMPTS_1, CONNSP_2, EUCLID, FUNCT_1,
      FUNCT_2, GOBOARD6, JORDAN24, JORDAN2C, ORDINAL1, PRE_TOPC, RELAT_1,
      RLVECT_1, SUBSET_1, TARSKI, TOPMETR, TOPREAL9, TOPRNS_1, TOPS_1, TOPS_2,
      XBOOLE_0, XBOOLE_1, XREAL_0, XREAL_1, XXREAL_0, ZFMISC_1, CARD_1, TSEP_1,
      SETFAM_1, BROUWER2, NAT_1, TOPGRP_1, JORDAN, METRIZTS, T_0TOPSP,
      BORSUK_3, EUCLID_2, TOPREALA, FUNCT_3, EQREL_1, TIETZE_2, CONNSP_1,
      CONNSP_3, CARD_2, WAYBEL23, YELLOW12, BROUWER3,JGRAPH_1,TOPS_4;
 schemes FUNCT_2, NAT_1, CLASSES1;

begin :: Preliminaries

 reserve n,m for Nat,
         p,q for Point of TOP-REAL n, r for Real;

theorem Th1: :: MFOLD_1:1
  for T being 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 being 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,def 3;
    A5: for x being 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;
  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_1:4
  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 Th3: ::MFOLD_1:9
  for r,s being 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,19;
  A10:Ball(p,r) \/ Sphere(p,r) = cl_Ball(p,r)& Ball(p,r) misses Sphere(p,r)
      by TOPREAL9:18,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,19;
  A14:Ball(p,r) \/ Sphere(p,r) = cl_Ball(p,r) &
  Ball(p,r) misses Sphere(p,r) by TOPREAL9:18,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
      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
  for M be non empty TopSpace
    for q be Point of M,r be real number,p be Point of TOP-REAL n st r>0
    for U be a_neighborhood of q st M|U,Tball(p,r) are_homeomorphic
    ex W being 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 :: Locally Euclidean Spaces

reserve M,M1,M2 for non empty TopSpace;

definition
  let M;
  attr M is locally_euclidean means :Def2:
    for p being Point of M
      ex U being a_neighborhood of p, n st
        M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic;
end;

definition
  let n,M;
  attr M is n-locally_euclidean means :Def3:
    for p being Point of M
      ex U being 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 :: Locally Euclidean Spaces With and Without a Boundary

definition
  let M be non empty TopSpace;
  func Int M -> Subset of M means :Def4:
    for p be Point of M holds
        p in it
      iff
        ex U being a_neighborhood of p, n st
          M|U,Tball(0.TOP-REAL n,1) are_homeomorphic;
  existence
  proof
    set I = {p where p is Point of M:ex U being 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 being 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 being a_neighborhood of q, n st
        M|U,Tball(0.TOP-REAL n,1) are_homeomorphic;
      hence ex U being 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 being 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 being 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 being 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 being 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,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;
  func Fr M -> Subset of M equals (Int M)`;
  coherence;
end;

::$N Boundary Points of Locally Euclidean Spaces
theorem Th5:
  for M be locally_euclidean non empty TopSpace
    for p be Point of M holds
        p in Fr M
     iff
        ex U being 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,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 :: Interior and Boundary of Locally Euclidean Spaces

definition
  let M be non empty TopSpace;
  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 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 ex U being 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 being 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 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 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_boundary n-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;

:: Correspondence between Classical and Extended Concepts
:: of Locally Euclidean Spaces
theorem
  M is without_boundary locally_euclidean non empty TopSpace
    iff
  for p be Point of M
    ex U be a_neighborhood of p,n st
      M|U,Tball(0.TOP-REAL n,1) are_homeomorphic
proof
  thus M is without_boundary locally_euclidean non empty TopSpace implies
   for p be Point of M ex U be a_neighborhood of p,n st
     M|U,Tball(0.TOP-REAL n,1) are_homeomorphic
  proof
    assume M is without_boundary locally_euclidean non empty TopSpace;
    hence thesis by Lm2;
  end;
  thus thesis by Lm2;
end;

theorem Th7:
  for M be with_boundary locally_euclidean non empty TopSpace
    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
        ex U being 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,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
     for p be Point of M|Int M
       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) 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) 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
    for p be Point of M
    for pM be Point of M|Fr M st p=pM
    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)
      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 :: Cartesian Product of Locally Euclidean Spaces

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 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 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 :: Fixed Dimension Locally Euclidean Spaces

definition
  let n;
  let M be n-locally_euclidean non empty TopSpace;
  redefine func Int M -> Subset of M means :Def7:
    for p be Point of M holds
      p in it
    iff
      ex U being 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 being
    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 being 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 being 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 being 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;
  redefine func Fr M -> Subset of M means
    for p be Point of M holds
      p in it
    iff
      ex U being 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 being
      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 being 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 being 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 being 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
  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 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;

::$N Topological Invariance of Dimension of Locally Euclidean Spaces
theorem
  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 Th13:
  M is without_boundary n-locally_euclidean non empty TopSpace
    iff
  for p be Point of M 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_boundary n-locally_euclidean non empty TopSpace;
    then reconsider MM=M as without_boundary n-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 ex U being 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 being 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;

::$N Dimension of the Cartesian Product of Locally Euclidean Spaces
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;

::$N Dimension of the Interior of Locally Euclidean Spaces
registration
  let n;
  let M be n-locally_euclidean non empty TopSpace;
  cluster M|Int M -> n-locally_euclidean for non empty TopSpace;
  coherence
  proof
    set MI=M|Int M;
A1: [#]MI=Int M by PRE_TOPC:def 5;
    for p be Point of MI ex U being 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;

::$N Dimension of the Boundary of Locally Euclidean Spaces
registration
  let n be non zero Nat;
  let M be with_boundary n-locally_euclidean non empty TopSpace;
  cluster M|Fr M -> (n-'1)-locally_euclidean for non empty TopSpace;
  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 being 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 :: Connected Components of Locally Euclidean Spaces

theorem Th14:
  for M be compact locally_euclidean non empty TopSpace
    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 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 is 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 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 being Point of MC 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
  for M be compact locally_euclidean non empty TopSpace
    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 is 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
  for M be compact locally_euclidean non empty TopSpace st
     M is connected
  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 :: Topological Manifold

registration
  let n;
  cluster second-countable Hausdorff n-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;