let n be Nat; :: thesis: for M, N being non empty TopSpace st M is n -manifold & M,N are_homeomorphic holds
N is n -manifold
let M, N be non empty TopSpace; :: thesis: ( M is n -manifold & M,N are_homeomorphic implies N is n -manifold )
assume A1: M is n -manifold ; :: thesis: ( not M,N are_homeomorphic or N is n -manifold )
assume A2: M,N are_homeomorphic ; :: thesis: N is n -manifold
then A3: N is second-countable by A1, Th9;
A4: N is Hausdorff by A1, A2, Th10;
N is n -locally_euclidean by A1, A2, MFOLD_0:10, MFOLD_0:11;
hence N is n -manifold by A3, A4; :: thesis: verum