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: (1 / 2) * (G . (a,a)) = (1 / 2) * 0 by A1, PCOMPS_1:def 6;
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 6 ;
hence 0 <= G . (a,b) by A1, A2, PCOMPS_1:def 6; :: thesis: verum