let X be non empty strict MetrSpace; :: thesis: ( the distance of X is Reflexive & the distance of X is discerning & the distance of X is symmetric & the distance of X is triangle )
A1: the distance of X is_metric_of the carrier of X by PCOMPS_1:35;
hence the distance of X is Reflexive by Th3; :: thesis: ( the distance of X is discerning & the distance of X is symmetric & the distance of X is triangle )
thus the distance of X is discerning by A1, Th3; :: thesis: ( the distance of X is symmetric & the distance of X is triangle )
thus the distance of X is symmetric by A1, Th3; :: thesis: the distance of X is triangle
thus the distance of X is triangle by A1, Th3; :: thesis: verum