consider f being object such that
A1: f in Mor C by XBOOLE_0:def 1;
reconsider f = f as morphism of C by A1;
consider c being morphism of C such that
A2: ( c |> f & c is left_identity ) by Def12, Def6;
c is identity by A2, Th9;
then c in { u where u is morphism of C : ( u is identity & u in Mor C ) } ;
hence not Ob C is empty ; :: thesis: verum