:: deftheorem defines is_a_unity_wrt BINOP_1:def 7 :
for A being set
for e being object
for o being BinOp of A holds
( e is_a_unity_wrt o iff ( e is_a_left_unity_wrt o & e is_a_right_unity_wrt o ) );