reconsider M = MetrStruct(# 1,Empty^2-to-zero #) as non empty strict MetrStruct ;
take M ; :: thesis: ( M is strict & M is Reflexive & M is discerning & M is symmetric & M is triangle & not M is empty )
( M is Reflexive & M is discerning & M is symmetric & M is triangle )

proof

thus the distance of M is Reflexive :: according to METRIC_1:def 7 :: thesis: ( M is discerning & M is symmetric & M is triangle )

proof

let a be Element of M; :: according to METRIC_1:def 3 :: thesis: the distance of M . a,a = 0
thus the distance of M . a,a = 0 by Lm3; :: thesis: verum

end;

thus the distance of M is discerning :: according to METRIC_1:def 8 :: thesis: ( M is symmetric & M is triangle )

proof

let a, b be Element of M; :: according to METRIC_1:def 4 :: thesis: ( the distance of M . a,b = 0 implies a = b )
assume the distance of M . a,b = 0 ; :: thesis: a = b
hence a = b by Lm3; :: thesis: verum

end;

thus the distance of M is symmetric :: according to METRIC_1:def 9 :: thesis: M is triangle

proof

let a, b be Element of M; :: according to METRIC_1:def 5 :: thesis: the distance of M . a,b = the distance of M . b,a
thus the distance of M . a,b = the distance of M . b,a by Lm4; :: thesis: verum

end;

thus the distance of M is triangle :: according to METRIC_1:def 10 :: thesis: verum

proof

let a, b, c be Element of M; :: according to METRIC_1:def 6 :: thesis: the distance of M . a,c <= (the distance of M . a,b) + (the distance of M . b,c)
thus the distance of M . a,c <= (the distance of M . a,b) + (the distance of M . b,c) by Lm5; :: thesis: verum

end;

end;

hence ( M is strict & M is Reflexive & M is discerning & M is symmetric & M is triangle & not M is empty ) ; :: thesis: verum