take {} N ; :: thesis: {} N is bounded
thus {} N is bounded ; :: thesis: verum