reconsider T = Tball ((0. (TOP-REAL n)),1) as topological_manifold ;
T is without_boundary ;
hence ex b₁ being topological_manifold st
( b₁ is n -dimensional & b₁ is without_boundary ) ; :: thesis: verum