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 :: thesis: 0 <= dist (a,b)

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

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

hence 0 <= dist (a,b) by Th1; :: thesis: verum

end;

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

hence 0 <= dist (a,b) by Th25; :: thesis: verum

end;

end;

end;

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