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