let M be non empty TopSpace; ( M is n -locally_euclidean implies M is infinite )
set TR = TOP-REAL n;
assume A8:
M is n -locally_euclidean
; M is infinite
consider p being object such that
A9:
p in the carrier of M
by XBOOLE_0:def 1;
reconsider p = p as Point of M by A9;
consider U being a_neighborhood of p such that
A10:
M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
by A8, MFOLD_0:def 3;
consider f being Function of (Tdisk ((0. (TOP-REAL n)),1)),(M | U) such that
A11:
f is being_homeomorphism
by A10, T_0TOPSP:def 1;
C:
[#] (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1)
by PRE_TOPC:def 5;
A12:
( dom f = [#] (Tdisk ((0. (TOP-REAL n)),1)) & rng f = [#] (M | U) & f is one-to-one )
by A11, TOPS_2:58;
( not Ball ((0. (TOP-REAL n)),1) is empty & Ball ((0. (TOP-REAL n)),1) is ball )
by MFOLD_1:def 1;
then
(TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1)),(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic
by MFOLD_1:10, METRIZTS:def 1;
then consider g being Function of ((TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1))),((TOP-REAL n) | ([#] (TOP-REAL n))) such that
B11:
g is being_homeomorphism
;
B12:
( dom g = [#] ((TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1))) & rng g = [#] ((TOP-REAL n) | ([#] (TOP-REAL n))) & g is one-to-one )
by B11, TOPS_2:58;
( Ball ((0. (TOP-REAL n)),1) is infinite & Ball ((0. (TOP-REAL n)),1) c= cl_Ball ((0. (TOP-REAL n)),1) )
by B12, PRE_TOPC:def 5, TOPREAL9:16;
then
[#] (Tdisk ((0. (TOP-REAL n)),1)) is infinite
by C;
hence
M is infinite
by A12, CARD_1:59; verum