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