:: deftheorem defines add_End LMOD_XX1:def 3 :
for M being AbGroup holds add_End M = (ADD (M,M)) | [:(set_End M),(set_End M):];