let C be strict Category; :: thesis: for A being strict Subcategory of C st the carrier of A = the carrier of C & the carrier' of A = the carrier' of C holds
A = C
let A be strict Subcategory of C; :: thesis: ( the carrier of A = the carrier of C & the carrier' of A = the carrier' of C implies A = C )
assume that
A1: the carrier of A = the carrier of C and
A2: the carrier' of A = the carrier' of C ; :: thesis: A = C
A3: the Target of A = the Target of C | the carrier' of A by Th4
.= the Target of C by A2 ;
A4: the Comp of A = the Comp of C || the carrier' of A by Th4
.= the Comp of C by A2 ;
the Source of A = the Source of C | the carrier' of A by Th4
.= the Source of C by A2 ;
hence A = C by A1, A3, A4; :: thesis: verum