( addMagma(# REAL,addreal #) is addGroup-like & addMagma(# REAL,addreal #) is add-associative ) by Lm1;
hence ex b₁ being addMagma st
( b₁ is strict & b₁ is addGroup-like & b₁ is add-associative & not b₁ is empty ) ; :: thesis: verum