for M being MetrStruct
for a being Point of M
for X being non empty set holds
( ( well_dist (a,X) is Reflexive implies M is Reflexive ) & ( well_dist (a,X) is symmetric implies M is symmetric ) & ( well_dist (a,X) is triangle & well_dist (a,X) is Reflexive implies M is triangle ) & ( well_dist (a,X) is discerning & well_dist (a,X) is Reflexive implies M is discerning ) )