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