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