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

now

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 Th14, METRIC_1:1; :: 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)
thus dist x,z <= (dist x,y) + (dist y,z) :: thesis: verum

proof

A1: dist x,z <= max (dist x,y),(dist y,z) by Def4;
( 0 <= dist x,y & 0 <= dist y,z ) by Th18;
then max (dist x,y),(dist y,z) <= (dist x,y) + (dist y,z) by Th1;
hence dist x,z <= (dist x,y) + (dist y,z) by A1, XXREAL_0:2; :: thesis: verum

end;

end;

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