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 set ; :: 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 a' = dom f, b' = cod f as Object of C by Th12;
( f in Hom (dom f),(cod f) & Hom (dom f),(cod f) c= Hom a',b' ) by Def4;
then f is Morphism of a',b' by CAT_1:21;
hence x in the carrier' of C ; :: thesis: verum