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