per cases ( C is empty or not C is empty ) ;

suppose C is empty ; :: thesis: o is morphism of C

hence o is morphism of C ; :: thesis: verum

end;

suppose not C is empty ; :: thesis: o is morphism of C

then not Ob C is empty ;
then o in Ob C ;
hence o is morphism of C ; :: thesis: verum

end;

end;