let X be set ; :: thesis: for f being Function of [:X,X:],REAL st f is_metric_of X holds
f is_a_pseudometric_of X
let f be Function of [:X,X:],REAL ; :: thesis: ( f is_metric_of X implies f is_a_pseudometric_of X )
assume f is_metric_of X ; :: thesis: f is_a_pseudometric_of X
then for a, b, c being Element of X holds
( f . a,a = 0 & f . a,b = f . b,a & f . a,c <= (f . a,b) + (f . b,c) ) by PCOMPS_1:def 7;
then ( f is Reflexive & f is symmetric & f is triangle ) by METRIC_1:def 3, METRIC_1:def 5, METRIC_1:def 6;
hence f is_a_pseudometric_of X by NAGATA_1:def 10; :: thesis: verum