:: deftheorem defines ExampleRIFSpace ROUGHIF1:def 15 :
ExampleRIFSpace = DiscreteApproxSpace {1,2,3,4,5};