let M be non empty TopSpace; :: thesis: ( M is n -locally_euclidean implies M is infinite )
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: U, [#] (TOP-REAL n) are_homeomorphic by A8, MFOLD_1:13;
M | U,(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic by A10, METRIZTS:def 1;
then consider f being Function of ((TOP-REAL n) | ([#] (TOP-REAL n))),(M | U) such that
A11: f is being_homeomorphism by T_0TOPSP:def 1;
A12: ( dom f = [#] ((TOP-REAL n) | ([#] (TOP-REAL n))) & rng f = [#] (M | U) & f is one-to-one ) by A11, TOPS_2:58;
[#] ((TOP-REAL n) | ([#] (TOP-REAL n))) is infinite by PRE_TOPC:def 5;
hence M is infinite by A12, CARD_1:59; :: thesis: verum