:: deftheorem Def1 defines bool ZFMISC_1:def 1 :
for X, b₂ being set holds
( b₂ = bool X iff for Z being set holds
( Z in b₂ iff Z c= X ) );