take M0 = MetrStruct(# 1,Empty^2-to-zero #); :: thesis: ( M0 is strict & M0 is ultra & M0 is Reflexive & M0 is symmetric & M0 is Discerning & M0 is triangle )
M0 is ultra

proof

let x, y, z be Element of M0; :: according to METRIC_1:def 19 :: thesis: dist (x,z) <= max ((dist (x,y)),(dist (y,z)))
thus dist (x,z) <= max ((dist (x,y)),(dist (y,z))) by Th25; :: thesis: verum

end;

hence ( M0 is strict & M0 is ultra & M0 is Reflexive & M0 is symmetric & M0 is Discerning & M0 is triangle ) ; :: thesis: verum