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 for a being Element of A holds G . (a,a) = 0 by PCOMPS_1:def 6;
hence G is Reflexive by METRIC_1:def 2; :: thesis: ( G is discerning & G is symmetric & G is triangle )
for a, b being Element of A holds
( G . (a,b) = 0 iff a = b ) by A2, PCOMPS_1:def 6;
hence G is discerning by METRIC_1:def 3; :: 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 6;
hence G is symmetric by METRIC_1:def 4; :: 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 6;
hence G is triangle by METRIC_1:def 5; :: thesis: verum
end;
( G is Reflexive & G is discerning & G is symmetric & G is triangle implies G is_metric_of A )
proof
assume ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) ; :: thesis: G is_metric_of A
then 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 METRIC_1:def 2, METRIC_1:def 3, METRIC_1:def 4, METRIC_1:def 5;
hence G is_metric_of A by PCOMPS_1:def 6; :: 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