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