thus ( not C is empty implies ex o being Object of C ex f1 being morphism of C st
( o = f1 & f |> f1 & f1 is identity ) ) :: thesis:

assume A1: not C is empty ; :: thesis:
then consider f1 being morphism of C such that
A2: ( f |> f1 & f1 is identity ) by Lm2;
reconsider o = f1 as Object of C by A2, A1, Th22;
take o ; :: thesis:
take f1 ; :: thesis:
thus ( o = f1 & f |> f1 & f1 is identity ) by A2; :: thesis:

end;