theorem Th18: :: CAT_8:18

ex f1, f2 being morphism of (OrdC 3) st
( not f1 is identity & not f2 is identity & cod f1 = dom f2 & Ob (OrdC 3) = {(dom f1),(cod f1),(cod f2)} & Mor (OrdC 3) = {(dom f1),(cod f1),(cod f2),f1,f2,(f2 (*) f1)} & dom f1, cod f1, cod f2,f1,f2,f2 (*) f1 are_mutually_distinct )