reconsider e = x as Point of (Euclid n) by TOPREAL3:8;
n in NAT by ORDINAL1:def 12;
then Ball (x,r) = Ball (e,r) by Th13;
hence not Ball (x,r) is empty by GOBOARD6:1; :: thesis: verum