take idm o ; :: thesis: ( idm o is mono & idm o is epi & idm o is retraction & idm o is coretraction )
thus ( idm o is mono & idm o is epi & idm o is retraction & idm o is coretraction ) by Lm1, Th1; :: thesis: verum