take M = Tdisk ((0. (TOP-REAL n)),1); :: thesis: ( M is with_boundary & M is compact )
thus ( M is with_boundary & M is compact ) ; :: thesis: verum