take TOP-REAL n ; :: thesis: TOP-REAL n is n -manifold
thus TOP-REAL n is n -manifold by Def5; :: thesis: verum