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