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, a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of C c= the Comp of C & ( for a, a9 being Object of C st a = a9 holds
id a = id a9 ) )
thus ( ( for a, b, a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of C c= the Comp of C & ( for a, a9 being Object of C st a = a9 holds
id a = id a9 ) ) ; :: thesis: verum