:: deftheorem defines having_a_unity SETWISEO:def 2 :
for X being non empty set
for F being BinOp of X holds
( F is having_a_unity iff ex x being Element of X st x is_a_unity_wrt F );