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