let C be CategoryStr ; :: thesis: for f being morphism of C st not C is empty holds

f in the carrier of C

let f be morphism of C; :: thesis: ( not C is empty implies f in the carrier of C )

assume not C is empty ; :: thesis: f in the carrier of C

then f in Mor C by SUBSET_1:def 1;

hence f in the carrier of C by CAT_6:def 1; :: thesis: verum

f in the carrier of C

let f be morphism of C; :: thesis: ( not C is empty implies f in the carrier of C )

assume not C is empty ; :: thesis: f in the carrier of C

then f in Mor C by SUBSET_1:def 1;

hence f in the carrier of C by CAT_6:def 1; :: thesis: verum