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