let A be non empty set ; :: thesis: for G being Function of [:A,A:],REAL st G is_metric_of A holds
for a, b being Element of A holds 0 <= G . a,b
let G be Function of [:A,A:],REAL ; :: thesis: ( G is_metric_of A implies for a, b being Element of A holds 0 <= G . a,b )
assume A1: G is_metric_of A ; :: thesis: for a, b being Element of A holds 0 <= G . a,b
let a, b be Element of A; :: thesis: 0 <= G . a,b
A2: G . a,a <= (G . a,b) + (G . b,a) by A1, PCOMPS_1:def 7;
A3: G . a,b = (1 / 2) * ((1 * (G . a,b)) + (G . a,b))
.= (1 / 2) * ((G . a,b) + (G . b,a)) by A1, PCOMPS_1:def 7 ;
(1 / 2) * (G . a,a) = (1 / 2) * 0 by A1, PCOMPS_1:def 7;
hence 0 <= G . a,b by A2, A3; :: thesis: verum