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:66; :: thesis: verum