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