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