let M be non empty Reflexive Discerning 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

now

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: 0 <= dist a,b

hence 0 <= dist a,b by METRIC_1:1; :: thesis: verum

end;

suppose a <> b ; :: thesis: 0 <= dist a,b

hence 0 <= dist a,b by Th14; :: thesis: verum

end;

end;

end;

hence 0 <= dist a,b ; :: thesis: verum