reconsider S = Ball ((0. (TOP-REAL n)),1) as ball Subset of (TOP-REAL n) by Def1;
take S ; :: thesis: ( not S is empty & S is ball )
thus ( not S is empty & S is ball ) ; :: thesis: verum