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