A1: now

let x, y be Element of MetrStruct(# 1,Empty^2-to-zero #); :: thesis: dist x,y = dist y,x
thus dist x,y = Empty^2-to-zero . x,y by METRIC_1:def 1
.= Empty^2-to-zero . y,x by Th6
.= dist y,x by METRIC_1:def 1 ; :: thesis: verum

end;

A2: now

let x, y be Element of MetrStruct(# 1,Empty^2-to-zero #); :: thesis: ( x <> y implies 0 < dist x,y )
A3: dist x,y = Empty^2-to-zero . x,y by METRIC_1:def 1;
assume x <> y ; :: thesis: 0 < dist x,y
hence 0 < dist x,y by A3, Th5; :: thesis: verum

end;

A4: now

let x, y, z be Element of MetrStruct(# 1,Empty^2-to-zero #); :: thesis: dist x,z <= (dist x,y) + (dist y,z)
( dist x,y = Empty^2-to-zero . x,y & dist x,z = Empty^2-to-zero . x,z & dist y,z = Empty^2-to-zero . y,z ) by METRIC_1:def 1;
hence dist x,z <= (dist x,y) + (dist y,z) by Th7; :: thesis: verum

end;

now

let x be Element of MetrStruct(# 1,Empty^2-to-zero #); :: thesis: dist x,x = 0
thus dist x,x = Empty^2-to-zero . x,x by METRIC_1:def 1
.= 0 by Th4 ; :: thesis: verum

end;

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 A1, A2, A4, Th14, METRIC_1:1, METRIC_1:3, METRIC_1:4; :: thesis: verum