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: dist a,a <= (dist a,b) + (dist b,a) by Th4;
A2: dist a,b = (1 / 2) * ((1 * (dist a,b)) + (1 * (dist a,b))) ;
(1 / 2) * (dist a,a) = (1 / 2) * 0 by Th1;
hence 0 <= dist a,b by A1, A2, XREAL_1:66; :: thesis: verum