theorem Th3: :: METRIC_6:3

for A being non empty set
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 ) )