:: deftheorem defines chi MONOID_1:def 5 :
for A being non empty set
for a being Element of A holds chi a = chi ({a},A);