take [#] X ; :: thesis: not [#] X is trivial
thus not [#] X is trivial ; :: thesis: verum