theorem :: BSPACE:14

for x being set holds {} @ x = 0. Z_2 by Def3;