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 object ; :: 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;
A3: y1 is Object of D by A1;
y2 is Object of D by A1;
then [[y1,y2],F] is Morphism of D by A3, Def8;
hence x in the carrier' of D by A2; :: thesis: verum

end;

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