let C be Categorial Category; :: thesis: for D being Categorial full Category st the carrier of C c= the carrier of D holds
C is Subcategory of D
let D be Categorial full Category; :: thesis: ( the carrier of C c= the carrier of D implies C is Subcategory of D )
assume A1: the carrier of C c= the carrier of D ; :: thesis: C is Subcategory of D
the carrier' of C c= the carrier' of D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of C or x in the carrier' of D )
assume x in the carrier' of C ; :: thesis: x in the carrier' of D
then reconsider x = x as Morphism of C ;
reconsider y1 = dom x, y2 = cod x as Category by Th12;
consider F being Functor of y1,y2 such that
A2: x = [[y1,y2],F] by Def6;
( y1 is Object of D & y2 is Object of D ) by A1, TARSKI:def 3;
then [[y1,y2],F] is Morphism of D by Def8;
hence x in the carrier' of D by A2; :: thesis: verum

end;

hence C is Subcategory of D by Th15; :: thesis: verum