let C be Category; :: thesis: for D being Subcategory of C
for E being Subcategory of D holds E is Subcategory of C
let D be Subcategory of C; :: thesis: for E being Subcategory of D holds E is Subcategory of C
let E be Subcategory of D; :: thesis: 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, XBOOLE_1:1; :: according to CAT_2:def 4 :: thesis: ( ( for b₁, b₂ being Element of the carrier of E
for b₃, b₄ being Element of the carrier of C holds
( not b₁ = b₃ or not b₂ = b₄ or Hom b₁,b₂ c= Hom b₃,b₄ ) ) & the Comp of E c= the Comp of C & ( for b₁ being Element of the carrier of E
for b₂ being Element of the carrier of C holds
( not b₁ = b₂ or id b₁ = id b₂ ) ) )

hereby :: thesis: ( the Comp of E c= the Comp of C & ( for b₁ being Element of the carrier of E
for b₂ being Element of the carrier of C holds
( not b₁ = b₂ or id b₁ = id b₂ ) ) )

let a, b be Object of E; :: thesis: 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; :: thesis: ( a = a9 & b = b9 implies Hom a,b c= Hom a9,b9 )
reconsider a1 = a, b1 = b as Object of D by CAT_2:12;
assume that
A5: a = a9 and
A6: b = b9 ; :: thesis: 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, XBOOLE_1:1; :: thesis: verum

end;

thus the Comp of E c= the Comp of C by A2, A4, XBOOLE_1:1; :: thesis: for b₁ being Element of the carrier of E
for b₂ being Element of the carrier of C holds
( not b₁ = b₂ or id b₁ = id b₂ )
let a be Object of E; :: thesis: for b₁ being Element of the carrier of C holds
( not a = b₁ or id a = id b₁ )
let a9 be Object of C; :: thesis: ( not a = a9 or id a = id a9 )
reconsider a1 = a as Object of D by CAT_2:12;
assume A8: a = a9 ; :: thesis: id a = id a9
id a = id a1 by CAT_2:def 4;
hence id a = id a9 by A8, CAT_2:def 4; :: thesis: verum