let X be set ; :: thesis: for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
for x, y being Element of X holds f . (x,y) >= 0
let f be Function of [:X,X:],REAL; :: thesis: ( f is_a_pseudometric_of X implies for x, y being Element of X holds f . (x,y) >= 0 )
assume A1: f is_a_pseudometric_of X ; :: thesis: for x, y being Element of X holds f . (x,y) >= 0
let x, y be Element of X; :: thesis: f . (x,y) >= 0
( f . (x,x) <= (f . (x,y)) + (f . (y,x)) & f . (x,x) = 0 ) by A1, Lm8;
then 0 <= ((f . (x,y)) + (f . (x,y))) / 2 by A1, Lm8;
hence f . (x,y) >= 0 ; :: thesis: verum