reconsider M = MetrStruct(# 1,Empty^2-to-zero #) as non empty strict MetrStruct ;
take
M
; ( 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
by Lm3;
A2:
the distance of M is symmetric
by Lm4;
A3:
the distance of M is triangle
by Lm5;
the distance of M is Reflexive
by Lm3;
hence
( M is strict & M is Reflexive & M is discerning & M is symmetric & M is triangle & not M is empty )
by A1, A2, A3; verum