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_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 A2: 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 A3: ( 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 A3, METRIC_1:def 6;
hence G . b,c <= (G . a,b) + (G . a,c) by A3, 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 A2, Th3; :: thesis: verum

end;

( 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
A4: ( G is Reflexive & G is discerning ) and
A5: for a, b, c being Element of A holds G . b,c <= (G . a,b) + (G . a,c) ; :: thesis: G is_metric_of A
A6: 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 . b,c <= (G . c,b) + (G . c,c) by A5;
then A7: G . b,c <= (G . c,b) + 0 by A4, METRIC_1:def 3;
G . c,b <= (G . b,c) + (G . b,b) by A5;
then G . c,b <= (G . b,c) + 0 by A4, METRIC_1:def 3;
hence G . b,c = G . c,b by A7, 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 A5;
hence G . a,c <= (G . a,b) + (G . b,c) by A6; :: thesis: verum

end;

then ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) by A4, A6, METRIC_1:def 5, METRIC_1:def 6;
hence G is_metric_of A by 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