theorem Th3: :: GROUP_1A:3
( addMagma(# REAL,addreal #) is add-associative & addMagma(# REAL,addreal #) is addGroup-like )