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

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