take +infty ; :: thesis: not +infty is natural
thus not +infty is natural ; :: thesis: verum