take {} ; :: thesis: {} is natural-valued
thus {} is natural-valued ; :: thesis: verum