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;