take Trivial-multLoopStr ; :: thesis: ( not Trivial-multLoopStr is empty & Trivial-multLoopStr is strict & Trivial-multLoopStr is AIM )
thus ( not Trivial-multLoopStr is empty & Trivial-multLoopStr is strict & Trivial-multLoopStr is AIM ) ; :: thesis: verum