let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for t1 being Element of T
for r being real number st r <= 0 holds
Ball t1,r = {}
let t1 be Element of T; :: thesis: for r being real number st r <= 0 holds
Ball t1,r = {}
let r be real number ; :: thesis: ( r <= 0 implies Ball t1,r = {} )
assume A1: r <= 0 ; :: thesis: Ball t1,r = {}
assume A2: Ball t1,r <> {} ; :: thesis: contradiction
consider c being Element of Ball t1,r;
reconsider c = c as Point of T by A2, TARSKI:def 3;
dist t1,c < r by A2, METRIC_1:12;
hence contradiction by A1, METRIC_1:5; :: thesis: verum