thus [#] (Tdisk x,r) is convex Subset of (TOP-REAL n) by Th3; :: according to TOPALG_2:def 1 :: thesis: verum