take T = Trivial-multLoopStr_0 ; :: thesis: ( T is almost_invertible & T is almost_cancelable & T is strict & not T is empty & T is trivial )
thus ( T is almost_invertible & T is almost_cancelable & T is strict & not T is empty & T is trivial ) ; :: thesis: verum