theorem Th39: :: CAT_7:39

ex f being morphism of (OrdC 2) st
( not f is identity & Ob (OrdC 2) = {(dom f),(cod f)} & Mor (OrdC 2) = {(dom f),(cod f),f} & dom f, cod f,f are_mutually_distinct )