take TOP-REAL 0 ; :: thesis: TOP-REAL 0 is manifold-like
thus TOP-REAL 0 is manifold-like ; :: thesis: verum