theorem :: BSPACE:19

for X being set
for c being Subset of X holds (1. Z_2) \*\ c = c by Def4;