:: deftheorem defines invertible LOPBAN_3:def 4 :
for X being non empty well-unital associative multLoopStr
for v being Element of X holds
( v is invertible iff ex w being Element of X st
( v * w = 1. X & w * v = 1. X ) );