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 :: thesis: ( S is add-associative & not S is empty )

proof

let x be Element of S; :: according to RLVECT_1:def 2 :: thesis: for w being Element of S holds x + w = w + x
thus for w being Element of S holds x + w = w + x by STRUCT_0:def 10; :: thesis: verum

end;

thus S is add-associative :: thesis: not S is empty

proof

let x be Element of S; :: according to RLVECT_1:def 3 :: thesis: for v, w being Element of S holds (x + v) + w = x + (v + w)
thus for v, w being Element of S holds (x + v) + w = x + (v + w) by STRUCT_0:def 10; :: thesis: verum

end;

thus not S is empty ; :: thesis: verum