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