A1:
for x being Element of MetrStruct(# 1,Empty^2-to-zero #) holds dist (x,x) = 0
by Lm3;
A2:
for x, y being Element of MetrStruct(# 1,Empty^2-to-zero #) holds dist (x,y) = dist (y,x)
by Th22;
A3:
for x, y being Element of MetrStruct(# 1,Empty^2-to-zero #) st x <> y holds
0 < dist (x,y)
by Th21;
for x, y, z being Element of MetrStruct(# 1,Empty^2-to-zero #) holds dist (x,z) <= (dist (x,y)) + (dist (y,z))
by Th23;
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 A2, A1, A3, Th25, Th1, Th3, Th4; verum