theorem Th6: :: MONOID_0:6

for G being non empty multMagma holds
( G is unital iff ex a being Element of G st
for b being Element of G holds
( a * b = b & b * a = b ) ) ;