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