A1:
for x, y, z being Element of MetrStruct(# 1,Empty^2-to-zero #) holds dist (x,z) <= (dist (x,y)) + (dist (y,z))
by Th7;
A3:
for x, y being Element of MetrStruct(# 1,Empty^2-to-zero #) st x <> y holds
0 < dist (x,y)
by Th5;
A5:
for x being Element of MetrStruct(# 1,Empty^2-to-zero #) holds dist (x,x) = 0
by Lm2;
for x, y being Element of MetrStruct(# 1,Empty^2-to-zero #) holds dist (x,y) = dist (y,x)
by Th6x;
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, Th1, Th3, Th4; verum