:: deftheorem Def2 defines { TARSKI:def 2 :
for y, z being object
for b₃ being set holds
( b₃ = {y,z} iff for x being object holds
( x in b₃ iff ( x = y or x = z ) ) );