let C be Category; :: thesis: C is Subcategory of C
thus the carrier of C c= the carrier of C ; :: according to CAT_2:def 4 :: thesis: ( ( for a, b, a', b' being Object of C st a = a' & b = b' holds
Hom a,b c= Hom a',b' ) & the Comp of C c= the Comp of C & ( for a, a' being Object of C st a = a' holds
id a = id a' ) )
thus ( ( for a, b, a', b' being Object of C st a = a' & b = b' holds
Hom a,b c= Hom a',b' ) & the Comp of C c= the Comp of C & ( for a, a' being Object of C st a = a' holds
id a = id a' ) ) ; :: thesis: verum