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