for X being non empty strict MetrSpace holds
( the distance of X is Reflexive & the distance of X is discerning & the distance of X is symmetric & the distance of X is triangle )