:: deftheorem defines { TARSKI:def 1 :
for y being object
for b₂ being set holds
( b₂ = {y} iff for x being object holds
( x in b₂ iff x = y ) );