theorem Th15: :: CAT_8:15

ex f being morphism of (OrdC 1) st
( f is identity & Ob (OrdC 1) = {f} & Mor (OrdC 1) = {f} )