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 20 :: thesis: dist x,z <= max (dist x,y),(dist y,z)
thus dist x,z <= max (dist x,y),(dist y,z) by Th8; :: thesis: verum

end;

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