consider M being non empty MetrSpace;
take TopSpaceMetr M ; :: thesis: ( TopSpaceMetr M is Hausdorff & not TopSpaceMetr M is empty & TopSpaceMetr M is strict )
thus ( TopSpaceMetr M is Hausdorff & not TopSpaceMetr M is empty & TopSpaceMetr M is strict ) by Th38; :: thesis: verum