set M = MetrStruct(# {{} ,{{} }},Set_to_zero #);

A1: now

let x, y, z be Element of MetrStruct(# {{} ,{{} }},Set_to_zero #); :: thesis: ( dist x,y = dist y,x & dist x,z <= (dist x,y) + (dist y,z) )
set x9 = x;
set y9 = y;
set z9 = z;
A2: dist x,y = Set_to_zero . x,y by METRIC_1:def 1;
dist y,x = Set_to_zero . y,x by METRIC_1:def 1;
hence dist x,y = dist y,x by A2, Th42; :: thesis: dist x,z <= (dist x,y) + (dist y,z)
( dist x,z = Set_to_zero . x,z & dist y,z = Set_to_zero . y,z ) by METRIC_1:def 1;
hence dist x,z <= (dist x,y) + (dist y,z) by A2, Th43; :: thesis: verum

end;

now

let x be Element of MetrStruct(# {{} ,{{} }},Set_to_zero #); :: thesis: dist x,x = 0
dist x,x = Set_to_zero . x,x by METRIC_1:def 1;
hence dist x,x = 0 by Th40; :: thesis: verum

end;

hence ( ZeroSpace is Reflexive & ZeroSpace is symmetric & ZeroSpace is triangle ) by A1, METRIC_1:1, METRIC_1:3, METRIC_1:4; :: thesis: verum