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 3 :: 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 4 :: 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 5 :: 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 2 :: 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