let r be real number ; :: thesis: for M being non empty Reflexive symmetric triangle MetrStruct
for z being Point of M st r < 0 holds
cl_Ball z,r = {}
let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for z being Point of M st r < 0 holds
cl_Ball z,r = {}
let z be Point of M; :: thesis: ( r < 0 implies cl_Ball z,r = {} )
assume r < 0 ; :: thesis: cl_Ball z,r = {}
then A1: ( Ball z,r = {} & Sphere z,r = {} ) by Th61, TBSP_1:17;
(Sphere z,r) \/ (Ball z,r) = cl_Ball z,r by METRIC_1:17;
hence cl_Ball z,r = {} by A1; :: thesis: verum