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) ;
|.(y - x).| <= r by A1, Th6;
hence contradiction ; :: thesis: verum