:: deftheorem defines invertible ALGSTR_0:def 33 :
for M being multLoopStr holds
( M is invertible iff ( M is right_invertible & M is left_invertible ) );