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
Sphere z,r = {}
let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for z being Point of M st r < 0 holds
Sphere z,r = {}
let z be Point of M; :: thesis: ( r < 0 implies Sphere z,r = {} )
assume A1: r < 0 ; :: thesis: Sphere z,r = {}
thus Sphere z,r c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= Sphere z,r

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Sphere z,r or a in {} )
assume A2: a in Sphere z,r ; :: thesis: a in {}
then reconsider b = a as Point of M ;
dist b,z = r by A2, METRIC_1:14;
hence a in {} by A1, METRIC_1:5; :: thesis: verum

end;

thus {} c= Sphere z,r by XBOOLE_1:2; :: thesis: verum