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