let C be Category; :: thesis: for E being Subcategory of C holds the carrier' of E c= the carrier' of C

let E be Subcategory of C; :: thesis: the carrier' of E c= the carrier' of C

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of E or x in the carrier' of C )

assume x in the carrier' of E ; :: thesis: x in the carrier' of C

then reconsider f = x as Morphism of E ;

set a = dom f;

set b = cod f;

reconsider a9 = dom f, b9 = cod f as Object of C by Th2;

( f in Hom ((dom f),(cod f)) & Hom ((dom f),(cod f)) c= Hom (a9,b9) ) by Def4;

then ( f in Hom (a9,b9) & Hom (a9,b9) <> {} ) ;

hence x in the carrier' of C ; :: thesis: verum

let E be Subcategory of C; :: thesis: the carrier' of E c= the carrier' of C

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of E or x in the carrier' of C )

assume x in the carrier' of E ; :: thesis: x in the carrier' of C

then reconsider f = x as Morphism of E ;

set a = dom f;

set b = cod f;

reconsider a9 = dom f, b9 = cod f as Object of C by Th2;

( f in Hom ((dom f),(cod f)) & Hom ((dom f),(cod f)) c= Hom (a9,b9) ) by Def4;

then ( f in Hom (a9,b9) & Hom (a9,b9) <> {} ) ;

hence x in the carrier' of C ; :: thesis: verum