Theorem bj-modssabl

Description: (The additive groups of) modules are abelian groups. (The elemental version is lmodabl ; see also lmodgrp and lmodcmn .) (Contributed by BJ, 9-Jun-2019)

	Ref	Expression
Assertion	bj-modssabl	|- LMod C_ Abel

Proof

Step	Hyp	Ref	Expression
1		lmodabl	|- ( x e. LMod -> x e. Abel )
2	1	ssriv	|- LMod C_ Abel