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