let M be UltraMetricSpace; :: thesis: ( M is triangle & M is discerning )

now :: thesis: for x, y, z being Element of M holds
( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )

let x, y, z be Element of M; :: thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
thus ( dist (x,y) = 0 iff x = y ) by Th25, Th1; :: thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
thus dist (x,y) = dist (y,x) ; :: thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
( 0 <= dist (x,y) & 0 <= dist (y,z) ) by Th26;
then A1: max ((dist (x,y)),(dist (y,z))) <= (dist (x,y)) + (dist (y,z)) by SQUARE_1:2;
dist (x,z) <= max ((dist (x,y)),(dist (y,z))) by Def19;
hence dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, XXREAL_0:2; :: thesis: verum

end;

hence ( M is triangle & M is discerning ) by Th6; :: thesis: verum