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