consider a being BinOp of {0 };
reconsider z = 0 as Element of {0 } by TARSKI:def 1;
take doubleLoopStr(# {0 },a,a,z,z #) ; :: thesis: ( doubleLoopStr(# {0 },a,a,z,z #) is strict & doubleLoopStr(# {0 },a,a,z,z #) is trivial & not doubleLoopStr(# {0 },a,a,z,z #) is empty )
thus ( doubleLoopStr(# {0 },a,a,z,z #) is strict & doubleLoopStr(# {0 },a,a,z,z #) is trivial & not doubleLoopStr(# {0 },a,a,z,z #) is empty ) ; :: thesis: verum