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