:: deftheorem defines bspace BSPACE:def 7 :
for X being set holds bspace X = ModuleStr(# (bool X),(bspace-sum X),({} X),(bspace-scalar-mult X) #);