let C be with_identities CategoryStr ; :: thesis: for a being Object of C st not C is empty holds
a in the carrier of C
let a be Object of C; :: thesis: ( not C is empty implies a in the carrier of C )
assume not C is empty ; :: thesis: a in the carrier of C
then a in Ob C by SUBSET_1:def 1;
then a in Mor C ;
hence a in the carrier of C by CAT_6:def 1; :: thesis: verum