:: deftheorem defines DiscreteApproxSpace ROUGHIF1:def 14 :
for X being set holds DiscreteApproxSpace X = RelStr(# X,(id X) #);