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

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