take 1TopSp {{}} ; :: thesis: ( 1TopSp {{}} is Hausdorff & not 1TopSp {{}} is empty )
thus ( 1TopSp {{}} is Hausdorff & not 1TopSp {{}} is empty ) ; :: thesis: verum