Second isomorphism theorem for subobjects in an abelian category, without refinements

To get y/(x⊓y) ≅ (x⊔y)/x for Subobject X in an abelian category: fix q = cokernel.π x.arrow. For any s, show x ⊓ s --ofLE--> s --factorThruImageSubobject (s.arrow ≫ q)--> imageSubobject (s.arrow ≫ q) is short exact. Exactness comes directly from KernelFork.IsLimit.ofι: lift t ↦ (x ⊓ s).factorThru (t ≫ s.arrow), where the factoring is inf_factors plus x being the kernel of q via Abelian.monoIsKernelOfCokernel. Then use hS.exact.gIsCokernel + coconePointUniqueUpToIso. Finally, imageSubobject (y.arrow ≫ q) = imageSubobject ((x⊔y).arrow ≫ q), since exists q preserves ⊔ (existsPullbackAdj.gc.l_sup) and kills x. Use Subobject.isoOfEq to transport. Inside namespace Subobject, write _root_.inf_le_right etc.