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