A1: n in NAT by ORDINAL1:def 13;
then |.(x - x).| = 0 by TOPRNS_1:29;
hence not cl_Ball (x,r) is empty by A1, Th8; :: thesis: verum