theorem Th6: :: GRCAT_1:6

comp Trivial-addLoopStr = op1