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

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