:: deftheorem defines invertible ALGSTR_0:def 29 :
for M being multLoopStr
for x being Element of M holds
( x is invertible iff ( x is right_invertible & x is left_invertible ) );