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

proof

let x, y, z be Element of MetrStruct(# 1,Empty^2-to-zero #); :: according to SUB_METR:def 4 :: thesis: dist x,z <= max (dist x,y),(dist y,z)
( dist x,y = Empty^2-to-zero . x,y & dist x,z = Empty^2-to-zero . x,z & dist y,z = Empty^2-to-zero . y,z ) by METRIC_1:def 1;
hence dist x,z <= max (dist x,y),(dist y,z) by Th8; :: thesis: verum

end;

hence ( MetrStruct(# 1,Empty^2-to-zero #) is strict & MetrStruct(# 1,Empty^2-to-zero #) is ultra & MetrStruct(# 1,Empty^2-to-zero #) is Reflexive & MetrStruct(# 1,Empty^2-to-zero #) is symmetric & MetrStruct(# 1,Empty^2-to-zero #) is Discerning ) ; :: thesis: verum