:: deftheorem Def5 defines bspace-sum BSPACE:def 5 :
for X being set
for b₂ being BinOp of (bool X) holds
( b₂ = bspace-sum X iff for c, d being Subset of X holds b₂ . (c,d) = c \+\ d );