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