let C be Category; :: thesis: for E being Subcategory of C holds
( E is_full_subcategory_of C iff incl E is full )
let E be Subcategory of C; :: thesis: ( E is_full_subcategory_of C iff incl E is full )
thus ( E is_full_subcategory_of C implies incl E is full ) :: thesis: ( incl E is full implies E is_full_subcategory_of C )

proof

assume E is_full_subcategory_of C ; :: thesis: incl E is full
then for a, b being Object of
for a', b' being Object of st a = a' & b = b' holds
Hom a,b = Hom a',b' by Def6;
hence incl E is full by Th25; :: thesis: verum

end;

assume incl E is full ; :: thesis: E is_full_subcategory_of C
hence ( E is Subcategory of C & ( for a, b being Object of
for a', b' being Object of st a = a' & b = b' holds
Hom a,b = Hom a',b' ) ) by Th25; :: according to CAT_2:def 6 :: thesis: verum