take M = Tball ((0. (TOP-REAL n)),1); :: thesis: M is without_boundary
thus M is without_boundary ; :: thesis: verum