let n be Nat; :: thesis: ( Tball ((0. (TOP-REAL n)),1) is n -locally_euclidean & Tball ((0. (TOP-REAL n)),1) 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
thus (Tball ((0. (TOP-REAL n)),1)) | CM, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by TSEP_1:93; :: 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 3 :: 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;
A5: p in Int U by CONNSP_2:def 1;
consider W being a_neighborhood of p, m being Nat 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 ex U being a_neighborhood of p st MM | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A6; :: thesis: verum

end;

hence ( Tball ((0. (TOP-REAL n)),1) is n -locally_euclidean & Tball ((0. (TOP-REAL n)),1) is without_boundary ) by A2, Lm2; :: thesis: verum