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