let M be non empty TopSpace; :: thesis: ( M is n -locally_euclidean implies M is infinite )
set TR = TOP-REAL n;
assume A8: M is n -locally_euclidean ; :: thesis: 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; :: thesis: verum