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
A65: the carrier of C1 = rng (Obj F) and
A66: rng F c= the carrier' of C1 and
A67: 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
A68: the carrier of C2 = rng (Obj F) and
A69: rng F c= the carrier' of C2 and
A70: 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
A71: C1 is Subcategory of C2 by A67, A68, A69;
C2 is Subcategory of C1 by A65, A66, A70;
hence C1 = C2 by A71, Th3; :: thesis: verum