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