take X --> 0 ; :: thesis: X --> 0 is natural-valued
thus X --> 0 is natural-valued ; :: thesis: verum