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 2;
G . (b,c) <= (G . (c,b)) + (G . (c,c)) by A3;
then G . (b,c) <= (G . (c,b)) + 0 by A2, METRIC_1:def 2;
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 4, METRIC_1:def 5;
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 :: thesis: for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c))

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 5;
hence G . (b,c) <= (G . (a,b)) + (G . (a,c)) by A7, METRIC_1:def 4; :: 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