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