let f be Function of [:X,X:],REAL; :: thesis: ( f is Reflexive & f is symmetric & f is triangle implies f is nonnegative-yielding )
assume AA: ( f is Reflexive & f is symmetric & f is triangle ) ; :: thesis: f is nonnegative-yielding

now :: thesis: for a, b being Element of X holds f . (a,b) >= 0

let a, b be Element of X; :: thesis: f . (a,b) >= 0
f . (a,a) <= (f . (a,b)) + (f . (b,a)) by AA, METRIC_1:def 5;
then 0 <= (f . (a,b)) + (f . (b,a)) by AA, METRIC_1:def 2;
then 0 <= (f . (a,b)) + (f . (a,b)) by AA, METRIC_1:def 4;
hence f . (a,b) >= 0 ; :: thesis: verum

end;

hence f is nonnegative-yielding ; :: thesis: verum