theorem Th9: :: NAGATA_2:9

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