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 ; :: thesis: for a', b' being Object of st a = a' & b = b' holds
Hom a,b c= Hom a',b'
let a', b' be Object of ; :: thesis: ( a = a' & b = b' implies Hom a,b c= Hom a',b' )
reconsider a1 = a, b1 = b as Object of by CAT_2:12;
assume that
A5: a = a' and
A6: b = b' ; :: thesis: Hom a,b c= Hom a',b'
A7: Hom a,b c= Hom a1,b1 by CAT_2:def 4;
Hom a1,b1 c= Hom a',b' by A5, A6, CAT_2:def 4;
hence Hom a,b c= Hom a',b' 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 ; :: thesis: for b₁ being Element of the carrier of C holds
( not a = b₁ or id a = id b₁ )
let a' be Object of ; :: thesis: ( not a = a' or id a = id a' )
reconsider a1 = a as Object of by CAT_2:12;
assume A8: a = a' ; :: thesis: id a = id a'
id a = id a1 by CAT_2:def 4;
hence id a = id a' by A8, CAT_2:def 4; :: thesis: verum