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