for X being set
for f being Function of [:X,X:],REAL st f is_metric_of X holds
f is_a_pseudometric_of X