let C be Category; for D being Subcategory of C
for E being Subcategory of D holds E is Subcategory of C
let D be Subcategory of C; for E being Subcategory of D holds E is Subcategory of C
let E be Subcategory of D; E is Subcategory of C
A1:
the carrier of D c= the carrier of C
by CAT_2:def 4;
A2:
the Comp of D c= the Comp of C
by CAT_2:def 4;
A3:
the carrier of E c= the carrier of D
by CAT_2:def 4;
A4:
the Comp of E c= the Comp of D
by CAT_2:def 4;
thus
the carrier of E c= the carrier of C
by A1, A3; CAT_2:def 4 ( ( for b1, b2 being Element of the carrier of E
for b3, b4 being Element of the carrier of C holds
( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of E c= the Comp of C & ( for b1 being Element of the carrier of E
for b2 being Element of the carrier of C holds
( not b1 = b2 or id b1 = id b2 ) ) )
hereby ( the Comp of E c= the Comp of C & ( for b1 being Element of the carrier of E
for b2 being Element of the carrier of C holds
( not b1 = b2 or id b1 = id b2 ) ) )
let a,
b be
Object of
E;
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9)let a9,
b9 be
Object of
C;
( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) )reconsider a1 =
a,
b1 =
b as
Object of
D by CAT_2:6;
assume that A5:
a = a9
and A6:
b = b9
;
Hom (a,b) c= Hom (a9,b9)A7:
Hom (
a,
b)
c= Hom (
a1,
b1)
by CAT_2:def 4;
Hom (
a1,
b1)
c= Hom (
a9,
b9)
by A5, A6, CAT_2:def 4;
hence
Hom (
a,
b)
c= Hom (
a9,
b9)
by A7;
verum
end;
thus
the Comp of E c= the Comp of C
by A2, A4; for b1 being Element of the carrier of E
for b2 being Element of the carrier of C holds
( not b1 = b2 or id b1 = id b2 )
let a be Object of E; for b1 being Element of the carrier of C holds
( not a = b1 or id a = id b1 )
let a9 be Object of C; ( not a = a9 or id a = id a9 )
reconsider a1 = a as Object of D by CAT_2:6;
assume A8:
a = a9
; id a = id a9
id a = id a1
by CAT_2:def 4;
hence
id a = id a9
by A8, CAT_2:def 4; verum