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