:: deftheorem defines Trivial-addMagma ALGSTR_0:def 2 :
Trivial-addMagma = addMagma(# {0},op2 #);