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