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