let f be Function of [:X,X:],REAL; ( f is Reflexive & f is symmetric & f is triangle implies f is V154() )
assume AA:
( f is Reflexive & f is symmetric & f is triangle )
; f is V154()
now for a, b being Element of X holds f . (a,b) >= 0 let a,
b be
Element of
X;
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
;
verum end;
hence
f is V154()
; verum