theorem :: GROUP_1A:41

addMagma(# REAL,addreal #) is Abelian addGroup