consider R being non empty trivial strict doubleLoopStr ;
take R ; :: thesis: ( R is strict & R is trivial )
thus ( R is strict & R is trivial ) ; :: thesis: verum