let C be Category; :: thesis: for E being Subcategory of C holds incl E is faithful
let E be Subcategory of C; :: thesis: incl E is faithful
let a, b be Object of E; :: according to CAT_1:def 27 :: thesis: ( Hom (a,b) = {} or for b₁, b₂ being Morphism of a,b holds
( not (incl E) . b₁ = (incl E) . b₂ or b₁ = b₂ ) )
assume Hom (a,b) <> {} ; :: thesis: for b₁, b₂ being Morphism of a,b holds
( not (incl E) . b₁ = (incl E) . b₂ or b₁ = b₂ )
let f1, f2 be Morphism of a,b; :: thesis: ( not (incl E) . f1 = (incl E) . f2 or f1 = f2 )
(incl E) . f1 = f1 by FUNCT_1:18;
hence ( not (incl E) . f1 = (incl E) . f2 or f1 = f2 ) by FUNCT_1:18; :: thesis: verum