:: deftheorem defines doubleton FOMODEL0:def 32 :
for a, b being set holds a doubleton b = {a} \/ {b};