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