take <*0 *> ; :: thesis: ( not <*0 *> is empty & <*0 *> is constant )
thus ( not <*0 *> is empty & <*0 *> is constant ) ; :: thesis: verum