:: deftheorem defines Trivial-addLoopStr CLASSES5:def 22 :
for x being object holds Trivial-addLoopStr x = addLoopStr(# {x},(op2 x),(op0 x) #);