theorem Th28: :: NAGATA_1:28

for X being set
for f being Function of [:X,X:],REAL holds
( f is_a_pseudometric_of X iff for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) )