set R = the non empty trivial strict doubleLoopStr ;
take the non empty trivial strict doubleLoopStr ; :: thesis: ( the non empty trivial strict doubleLoopStr is strict & the non empty trivial strict doubleLoopStr is trivial )
thus ( the non empty trivial strict doubleLoopStr is strict & the non empty trivial strict doubleLoopStr is trivial ) ; :: thesis: verum