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