let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for t1 being Element of T

for r being Real st r <= 0 holds

Ball (t1,r) = {}

let t1 be Element of T; :: thesis: for r being Real st r <= 0 holds

Ball (t1,r) = {}

let r be Real; :: thesis: ( r <= 0 implies Ball (t1,r) = {} )

assume A1: r <= 0 ; :: thesis: Ball (t1,r) = {}

set c = the Element of Ball (t1,r);

assume A2: Ball (t1,r) <> {} ; :: thesis: contradiction

then reconsider c = the Element of Ball (t1,r) as Point of T by TARSKI:def 3;

dist (t1,c) < r by A2, METRIC_1:11;

hence contradiction by A1, METRIC_1:5; :: thesis: verum

for r being Real st r <= 0 holds

Ball (t1,r) = {}

let t1 be Element of T; :: thesis: for r being Real st r <= 0 holds

Ball (t1,r) = {}

let r be Real; :: thesis: ( r <= 0 implies Ball (t1,r) = {} )

assume A1: r <= 0 ; :: thesis: Ball (t1,r) = {}

set c = the Element of Ball (t1,r);

assume A2: Ball (t1,r) <> {} ; :: thesis: contradiction

then reconsider c = the Element of Ball (t1,r) as Point of T by TARSKI:def 3;

dist (t1,c) < r by A2, METRIC_1:11;

hence contradiction by A1, METRIC_1:5; :: thesis: verum