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 Th28, Th29;
for x being Element of MetrStruct(# 2,Set_to_zero #) holds dist (x,x) = 0 by Th27;
hence ( ZeroSpace is Reflexive & ZeroSpace is symmetric & ZeroSpace is triangle ) by A1, Th1, Th3, Th4; :: thesis: verum