:: deftheorem Def4 defines \*\ BSPACE:def 4 :
for X being set
for a being Element of Z_2
for c being Subset of X holds
( ( a = 1. Z_2 implies a \*\ c = c ) & ( a = 0. Z_2 implies a \*\ c = {} X ) );