take Trivial-multLoopStr_0 ; :: thesis: ( Trivial-multLoopStr_0 is almost_cancelable & Trivial-multLoopStr_0 is strict & Trivial-multLoopStr_0 is 1 -element )
thus ( Trivial-multLoopStr_0 is almost_cancelable & Trivial-multLoopStr_0 is strict & Trivial-multLoopStr_0 is 1 -element ) ; :: thesis: verum