:: deftheorem defines -singleton AOFA_A00:def 1 :
for I being set
for i being Element of I
for x being set holds i -singleton x = (EmptyMS I) +* (i,{x});