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 & G is symmetric & G is triangle ) )
let G be Function of [:A,A:],REAL ; :: thesis: ( G is_metric_of A iff ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) )
A1: ( G is_metric_of A implies ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) )

proof

assume A2: G is_metric_of A ; :: thesis: ( G is Reflexive & G is discerning & G is symmetric & G is triangle )
then A3: for a, b being Element of A holds
( G . a,b = 0 iff a = b ) by PCOMPS_1:def 7;
for a being Element of A holds G . a,a = 0 by A2, PCOMPS_1:def 7;
hence G is Reflexive by METRIC_1:def 3; :: thesis: ( G is discerning & G is symmetric & G is triangle )
thus G is discerning by A3, METRIC_1:def 4; :: thesis: ( G is symmetric & G is triangle )
for a, b being Element of A holds G . a,b = G . b,a by A2, PCOMPS_1:def 7;
hence G is symmetric by METRIC_1:def 5; :: thesis: G is triangle
for a, b, c being Element of A holds G . a,c <= (G . a,b) + (G . b,c) by A2, PCOMPS_1:def 7;
hence G is triangle by METRIC_1:def 6; :: thesis: verum

end;

( G is Reflexive & G is discerning & G is symmetric & G is triangle implies G is_metric_of A )

proof

assume that
A4: ( G is Reflexive & G is discerning ) and
A5: G is symmetric and
A6: G is triangle ; :: thesis: G is_metric_of A
for a, b, c being Element of A holds
( ( G . a,b = 0 implies a = b ) & ( a = b implies G . a,b = 0 ) & G . a,b = G . b,a & G . a,c <= (G . a,b) + (G . b,c) ) by A4, A5, A6, METRIC_1:def 3, METRIC_1:def 4, METRIC_1:def 5, METRIC_1:def 6;
hence G is_metric_of A by PCOMPS_1:def 7; :: thesis: verum

end;

hence ( G is_metric_of A iff ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) ) by A1; :: thesis: verum