let X be non empty set ; :: thesis: for f being nonnegative-yielding Reflexive discerning triangle Function of [:X,X:],REAL
for x, y being Element of X st x <> y holds
f . (x,y) > 0
let f be nonnegative-yielding Reflexive discerning triangle Function of [:X,X:],REAL; :: thesis: for x, y being Element of X st x <> y holds
f . (x,y) > 0
let x, y be Element of X; :: thesis: ( x <> y implies f . (x,y) > 0 )
assume x <> y ; :: thesis: f . (x,y) > 0
then f . (x,y) <> 0 by METRIC_1:def 3;
hence f . (x,y) > 0 by Non; :: thesis: verum