take S = Trivial-addMagma ; :: thesis: ( S is strict & S is Abelian & S is add-associative & not S is empty )
thus S is strict ; :: thesis: ( S is Abelian & S is add-associative & not S is empty )
thus S is Abelian by STRUCT_0:def 10; :: thesis: ( S is add-associative & not S is empty )
thus S is add-associative by STRUCT_0:def 10; :: thesis: not S is empty
thus not S is empty ; :: thesis: verum