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