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

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