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) = {}
consider c being Element of Ball (t1,r);
assume A2: Ball (t1,r) <> {} ; :: thesis: contradiction
then reconsider c = c as Point of T by TARSKI:def 3;
dist (t1,c) < r by A2, METRIC_1:12;
hence contradiction by A1, METRIC_1:5; :: thesis: verum