theorem Th11: :: SETWISEO:14

for X being non empty set
for F being BinOp of X holds
( F is having_a_unity iff the_unity_wrt F is_a_unity_wrt F ) by BINOP_1:def 8;