take I = idm o; :: thesis: ( I is mono & I is epi & I is iso & I is retraction & I is coretraction )
( <^o,o^> <> {} & I is retraction & I is coretraction ) by Th1, ALTCAT_1:19;
hence ( I is mono & I is epi & I is iso & I is retraction & I is coretraction ) by Th15, Th16, Th20; :: thesis: verum