:: deftheorem defines # CLASSES5:def 36 :
for AbG being AbGroup holds # AbG = the addF of AbG;