take [#] S ; :: thesis: not [#] S is empty
thus not [#] S is empty ; :: thesis: verum