let n, m be Nat; :: thesis: for M being non empty TopSpace st M is n -locally_euclidean & M is m -locally_euclidean holds
n = m
let M be non empty TopSpace; :: thesis: ( M is n -locally_euclidean & M is m -locally_euclidean implies n = m )
assume that
A1: M is n -locally_euclidean and
A2: M is m -locally_euclidean ; :: thesis: n = m
set p = the Point of M;
consider W being a_neighborhood of the Point of M such that
A3: M | W, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by A2;
consider U being a_neighborhood of the Point of M such that
A4: M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A1;
A5: the Point of M in Int W by CONNSP_2:def 1;
the Point of M in Int U by CONNSP_2:def 1;
hence n = m by A5, XBOOLE_0:3, A4, A3, BROUWER3:14; :: thesis: verum