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