let X be set ; 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; ( 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
; for x, y being Element of X holds f . (x,y) >= 0
let x, y be Element of X; 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
; verum