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)) )

hence
( M is triangle & M is discerning )
by Th6; :: thesis: verum( ( 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;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