take TOP-REAL n ; :: thesis: ( TOP-REAL n is without_boundary & TOP-REAL n is n -manifold )
thus ( TOP-REAL n is without_boundary & TOP-REAL n is n -manifold ) ; :: thesis: verum