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

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