n in NAT by ORDINAL1:def 13;
hence Ball (x,r) is convex by Lm2; :: thesis: verum