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