let C be Category; :: thesis: for E being Subcategory of C
for e being Object of E holds e is Object of C
let E be Subcategory of C; :: thesis: for e being Object of E holds e is Object of C
let e be Object of E; :: thesis: e is Object of C
( e in the carrier of E & the carrier of E c= the carrier of C ) by Def4;
hence e is Object of C ; :: thesis: verum