Fix an abelian category and suppose $M',M,N',N$ are sub-objects of a given object such that $M'\subset M$ and $N'\subset N$. Then there exists a canonical isomorphism
$\frac{M'+(M\bigcap N)}{M'+(M\bigcap N')}=\frac{N'+(N\bigcap M)}{N'+(N\bigcap M')}$
By symmetry, it suffices to prove that
$\frac{M'+(M\bigcap N)}{M'+(M\bigcap N')}=\frac{M\bigcap N}{(M'\bigcap N)+(M\bigcap N')}$
However I need a technical result as follows
$(M'+(M\bigcap N'))\bigcap N=(M'\bigcap N)+(M\bigcap N')$
It is trivial that $(M'\bigcap N)+(M\bigcap N')\hookrightarrow(M'+(M\bigcap N'))\bigcap N$.
Does there exist a canonical inclusion of the other direction or is this trivial inclusion also epic? Positive answer to either will accomplish the proof. I appreciate a categorical proof due to aesthetic and concise considerations. However I'm not a perfectionist yet indeed very concerned about using the embedding theorem in that I don't really know why the existing monomorphism shown above when embedded in the category of modules is the one that I need to prove its own surjectivity! Maybe I didn't do my homework very well, so please let me know if anyone can resolve my doubt when the embedding theorem is availed of.
Furthermore, it is well known that the Zassenhaus Lemma is used to prove the Jordan-Holder theorem based on which the length of a module can be defined. Therefore I would be satisfied with the negative answer to the above question if the notion of length currently doesn't exist in other abelian categories such as the category of abelian sheaves or if such a notion can be defined via some other ways!
