theorem Th3: :: GROUP_1A:3

( addMagma(# REAL,addreal #) is add-associative & addMagma(# REAL,addreal #) is addGroup-like )