assume not Ball (x,r) is empty ; :: thesis: contradiction
then consider y being Point of (TOP-REAL n) such that
A1: y in Ball (x,r) by SUBSET_1:4;
n in NAT by ORDINAL1:def 12;
then |.(y - x).| < r by A1, Th7;
hence contradiction ; :: thesis: verum