let S be Subset of (TOP-REAL n); :: thesis: ( S is ball implies S is open )
assume S is ball ; :: thesis: S is open
then ex p being Point of (TOP-REAL n) ex r being real number st S = Ball (p,r) by Def1;
hence S is open ; :: thesis: verum