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

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