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 E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) 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 E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) ) ) by Th25; :: according to CAT_2:def 6 :: thesis: verum