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