n in NAT by ORDINAL1:def 13;
hence cl_Ball x,r is convex by Lm1; :: thesis: verum