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

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