theorem Th10: :: MONOID_0:10

for G being non empty multMagma holds
( G is invertible iff for a, b being Element of G ex r, l being Element of G st
( a * r = b & l * a = b ) )