for X being 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