:: deftheorem defines is_a_pseudometric_of NAGATA_1:def 10 :
for X being set
for f being Function of [:X,X:],REAL holds
( f is_a_pseudometric_of X iff ( f is Reflexive & f is symmetric & f is triangle ) );