take <*0 ,0 *> ; :: thesis: not <*0 ,0 *> is trivial
thus not <*0 ,0 *> is trivial ; :: thesis: verum