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