set M = MetrStruct(# 2,Set_to_zero #);
A1: for x, y, z being Element of MetrStruct(# 2,Set_to_zero #) holds
( dist x,y = dist y,x & dist x,z <= (dist x,y) + (dist y,z) ) by Th42, Th43;
for x being Element of MetrStruct(# 2,Set_to_zero #) holds dist x,x = 0 by Th40;
hence ( ZeroSpace is Reflexive & ZeroSpace is symmetric & ZeroSpace is triangle ) by A1, Th1, Th3, Th4; :: thesis: verum