Tball ((0. (TOP-REAL n)),1) = (TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1)) by MFOLD_1:def 2;
then 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