reconsider G = multMagma(# REAL,addreal #) as Group by GROUP_1:3;
take G ; :: thesis: ( G is strict & not G is trivial )
thus ( G is strict & not G is trivial ) ; :: thesis: verum