let A be non empty set ; :: thesis: for G being Function of [:A,A:],REAL holds
( G is_metric_of A iff ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . b,c <= (G . a,b) + (G . a,c) ) ) )
let G be Function of [:A,A:],REAL ; :: thesis: ( G is_metric_of A iff ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . b,c <= (G . a,b) + (G . a,c) ) ) )
A1: ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . b,c <= (G . a,b) + (G . a,c) ) implies G is_metric_of A )

proof

assume that
A2: ( G is Reflexive & G is discerning ) and
A3: for a, b, c being Element of A holds G . b,c <= (G . a,b) + (G . a,c) ; :: thesis: G is_metric_of A
A4: for b, c being Element of A holds G . b,c = G . c,b

proof

let b, c be Element of A; :: thesis: G . b,c = G . c,b
G . c,b <= (G . b,c) + (G . b,b) by A3;
then A5: G . c,b <= (G . b,c) + 0 by A2, METRIC_1:def 3;
G . b,c <= (G . c,b) + (G . c,c) by A3;
then G . b,c <= (G . c,b) + 0 by A2, METRIC_1:def 3;
hence G . b,c = G . c,b by A5, XXREAL_0:1; :: thesis: verum

end;

for a, b, c being Element of A holds G . a,c <= (G . a,b) + (G . b,c)

proof

let a, b, c be Element of A; :: thesis: G . a,c <= (G . a,b) + (G . b,c)
G . a,c <= (G . b,a) + (G . b,c) by A3;
hence G . a,c <= (G . a,b) + (G . b,c) by A4; :: thesis: verum

end;

then ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) by A2, A4, METRIC_1:def 5, METRIC_1:def 6;
hence G is_metric_of A by Th3; :: thesis: verum

end;

( G is_metric_of A implies ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . b,c <= (G . a,b) + (G . a,c) ) ) )

proof

assume A6: G is_metric_of A ; :: thesis: ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . b,c <= (G . a,b) + (G . a,c) ) )
then A7: ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) by Th3;

now

let a, b, c be Element of A; :: thesis: G . b,c <= (G . a,b) + (G . a,c)
G . b,c <= (G . b,a) + (G . a,c) by A7, METRIC_1:def 6;
hence G . b,c <= (G . a,b) + (G . a,c) by A7, METRIC_1:def 5; :: thesis: verum

end;

hence ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . b,c <= (G . a,b) + (G . a,c) ) ) by A6, Th3; :: thesis: verum

end;

hence ( G is_metric_of A iff ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . b,c <= (G . a,b) + (G . a,c) ) ) ) by A1; :: thesis: verum