let n be Nat; :: thesis: ( Tball ((0. (TOP-REAL n)),1) is n -locally_euclidean & ( for M1 being non empty n -locally_euclidean TopSpace st M1 = Tball ((0. (TOP-REAL n)),1) holds
M1 is without_boundary ) )
set TR = TOP-REAL n;
set M = Tball ((0. (TOP-REAL n)),1);
A1: for p being Point of (Tball ((0. (TOP-REAL n)),1)) ex U being a_neighborhood of p st (Tball ((0. (TOP-REAL n)),1)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

proof

let p be Point of (Tball ((0. (TOP-REAL n)),1)); :: thesis: ex U being a_neighborhood of p st (Tball ((0. (TOP-REAL n)),1)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
Int ([#] (Tball ((0. (TOP-REAL n)),1))) = [#] (Tball ((0. (TOP-REAL n)),1)) by TOPS_1:15;
then reconsider CM = [#] (Tball ((0. (TOP-REAL n)),1)) as non empty a_neighborhood of p by CONNSP_2:def 1;
take CM ; :: thesis: (Tball ((0. (TOP-REAL n)),1)) | CM, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
[#] ((Tball ((0. (TOP-REAL n)),1)) | CM) = CM by PRE_TOPC:def 5;
then reconsider cm = CM as non empty Subset of ((Tball ((0. (TOP-REAL n)),1)) | CM) ;
TopStruct(# the carrier of ((Tball ((0. (TOP-REAL n)),1)) | CM), the topology of ((Tball ((0. (TOP-REAL n)),1)) | CM) #), TopStruct(# the carrier of (Tball ((0. (TOP-REAL n)),1)), the topology of (Tball ((0. (TOP-REAL n)),1)) #) are_homeomorphic by TSEP_1:93;
hence (Tball ((0. (TOP-REAL n)),1)) | CM, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by TOPREALA:15; :: thesis: verum

end;

A2: for p being Point of (Tball ((0. (TOP-REAL n)),1)) ex U being a_neighborhood of p ex m being Nat st (Tball ((0. (TOP-REAL n)),1)) | U, Tball ((0. (TOP-REAL m)),1) are_homeomorphic

proof

let p be Point of (Tball ((0. (TOP-REAL n)),1)); :: thesis: ex U being a_neighborhood of p ex m being Nat st (Tball ((0. (TOP-REAL n)),1)) | U, Tball ((0. (TOP-REAL m)),1) are_homeomorphic
ex U being a_neighborhood of p st (Tball ((0. (TOP-REAL n)),1)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A1;
hence ex U being a_neighborhood of p ex m being Nat st (Tball ((0. (TOP-REAL n)),1)) | U, Tball ((0. (TOP-REAL m)),1) are_homeomorphic ; :: thesis: verum

end;

then reconsider MM = Tball ((0. (TOP-REAL n)),1) as non empty locally_euclidean TopSpace by Lm2;
MM is n -locally_euclidean

proof

let p be Point of MM; :: according to MFOLD_0:def 2 :: thesis: ex U being a_neighborhood of p st MM | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
consider U being a_neighborhood of p such that
A3: MM | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A1;
A: Tball ((0. (TOP-REAL n)),1) = (TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1)) by MFOLD_1:def 2;
A4: p in Int U by CONNSP_2:def 1;
consider W being a_neighborhood of p, m being Nat such that
A5: MM | W, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by Def1;
p in Int W by CONNSP_2:def 1;
then m = n by A4, XBOOLE_0:3, A3, A5, A, BROUWER3:15;
hence ex U being a_neighborhood of p st MM | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A5; :: thesis: verum

end;

hence Tball ((0. (TOP-REAL n)),1) is n -locally_euclidean ; :: thesis: for M1 being non empty n -locally_euclidean TopSpace st M1 = Tball ((0. (TOP-REAL n)),1) holds
M1 is without_boundary
let M1 be non empty n -locally_euclidean TopSpace; :: thesis: ( M1 = Tball ((0. (TOP-REAL n)),1) implies M1 is without_boundary )
thus ( M1 = Tball ((0. (TOP-REAL n)),1) implies M1 is without_boundary ) by A2, Lm2; :: thesis: verum