A1: now

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

end;

A3: now

let x, y be Element of MetrStruct(# 1,Empty^2-to-zero #); :: thesis: ( x <> y implies 0 < dist x,y )
assume A4: x <> y ; :: thesis: 0 < dist x,y
dist x,y = Empty^2-to-zero . x,y by METRIC_1:def 1;
hence 0 < dist x,y by A4, Th5; :: thesis: verum

end;

A5: now

let x be Element of MetrStruct(# 1,Empty^2-to-zero #); :: thesis: dist x,x = 0
thus dist x,x = Empty^2-to-zero . x,x by METRIC_1:def 1
.= 0 by Th4 ; :: thesis: verum

end;

now

let x, y be Element of MetrStruct(# 1,Empty^2-to-zero #); :: thesis: dist x,y = dist y,x
thus dist x,y = Empty^2-to-zero . x,y by METRIC_1:def 1
.= Empty^2-to-zero . y,x by Th6
.= dist y,x by METRIC_1:def 1 ; :: thesis: verum

end;

hence ( 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 triangle ) by A3, A1, A5, Th14, METRIC_1:1, METRIC_1:3, METRIC_1:4; :: thesis: verum