:: deftheorem Def3 defines @ BSPACE:def 3 :
for X being set
for x being object holds
( ( x in X implies X @ x = 1. Z_2 ) & ( not x in X implies X @ x = 0. Z_2 ) );