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