let C1, C2 be strict Subcategory of D; :: thesis: ( the carrier of C1 = rng (Obj F) & rng F c= the carrier' of C1 & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
C1 is Subcategory of E ) & the carrier of C2 = rng (Obj F) & rng F c= the carrier' of C2 & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
C2 is Subcategory of E ) implies C1 = C2 )
assume that
A35: ( the carrier of C1 = rng (Obj F) & rng F c= the carrier' of C1 ) and
A36: for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
C1 is Subcategory of E and
A37: ( the carrier of C2 = rng (Obj F) & rng F c= the carrier' of C2 ) and
A38: for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
C2 is Subcategory of E ; :: thesis: C1 = C2
( C1 is Subcategory of C2 & C2 is Subcategory of C1 ) by A35, A36, A37, A38;
hence C1 = C2 by Th3; :: thesis: verum