let M be Reflexive symmetric triangle MetrStruct ; :: thesis: for a, b being Element of M holds 0 <= dist (a,b)

let a, b be Element of M; :: thesis: 0 <= dist (a,b)

A1: (1 / 2) * (dist (a,a)) = (1 / 2) * 0 by Th1;

( dist (a,a) <= (dist (a,b)) + (dist (b,a)) & dist (a,b) = (1 / 2) * ((1 * (dist (a,b))) + (1 * (dist (a,b)))) ) by Th4;

hence 0 <= dist (a,b) by A1, XREAL_1:64; :: thesis: verum

let a, b be Element of M; :: thesis: 0 <= dist (a,b)

A1: (1 / 2) * (dist (a,a)) = (1 / 2) * 0 by Th1;

( dist (a,a) <= (dist (a,b)) + (dist (b,a)) & dist (a,b) = (1 / 2) * ((1 * (dist (a,b))) + (1 * (dist (a,b)))) ) by Th4;

hence 0 <= dist (a,b) by A1, XREAL_1:64; :: thesis: verum