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 )
A1: the distance of M is discerning

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 Lm2; :: thesis: verum

end;

A2: the distance of M is symmetric

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 Lm3; :: thesis: verum

end;

A3: the distance of M is triangle

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 Lm4; :: thesis: verum

end;

the distance of M is Reflexive

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 Lm2; :: thesis: verum

end;

hence ( M is strict & M is Reflexive & M is discerning & M is symmetric & M is triangle & not M is empty ) by A1, A2, A3, Def7, Def8, Def9, Def10; :: thesis: verum