let A be Category; :: thesis: for a being Object of A holds 1Cat a,(id a) is Subcategory of A
let d be Object of A; :: thesis: 1Cat d,(id d) is Subcategory of A
thus the carrier of (1Cat d,(id d)) c= the carrier of A :: according to CAT_2:def 4 :: thesis: ( ( for b₁, b₂ being Element of the carrier of (1Cat d,(id d))
for b₃, b₄ being Element of the carrier of A holds
( not b₁ = b₃ or not b₂ = b₄ or Hom b₁,b₂ c= Hom b₃,b₄ ) ) & the Comp of (1Cat d,(id d)) c= the Comp of A & ( for b₁ being Element of the carrier of (1Cat d,(id d))
for b₂ being Element of the carrier of A holds
( not b₁ = b₂ or id b₁ = id b₂ ) ) )

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in the carrier of (1Cat d,(id d)) or b in the carrier of A )
assume b in the carrier of (1Cat d,(id d)) ; :: thesis: b in the carrier of A
then b = d by TARSKI:def 1;
hence b in the carrier of A ; :: thesis: verum

end;

thus for a, b being Object of (1Cat d,(id d))
for a', b' being Object of A st a = a' & b = b' holds
Hom a,b c= Hom a',b' :: thesis: ( the Comp of (1Cat d,(id d)) c= the Comp of A & ( for b₁ being Element of the carrier of (1Cat d,(id d))
for b₂ being Element of the carrier of A holds
( not b₁ = b₂ or id b₁ = id b₂ ) ) )

proof

let a, b be Object of (1Cat d,(id d)); :: thesis: for a', b' being Object of A st a = a' & b = b' holds
Hom a,b c= Hom a',b'
let a', b' be Object of A; :: thesis: ( a = a' & b = b' implies Hom a,b c= Hom a',b' )
assume ( a = a' & b = b' ) ; :: thesis: Hom a,b c= Hom a',b'
then A1: ( a' = d & b' = d ) by TARSKI:def 1;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Hom a,b or x in Hom a',b' )
assume x in Hom a,b ; :: thesis: x in Hom a',b'
then x = id d by TARSKI:def 1;
hence x in Hom a',b' by A1, CAT_1:55; :: thesis: verum

end;

thus the Comp of (1Cat d,(id d)) c= the Comp of A :: thesis: for b₁ being Element of the carrier of (1Cat d,(id d))
for b₂ being Element of the carrier of A holds
( not b₁ = b₂ or id b₁ = id b₂ )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the Comp of (1Cat d,(id d)) or x in the Comp of A )
assume x in the Comp of (1Cat d,(id d)) ; :: thesis: x in the Comp of A
then x in {[[(id d),(id d)],(id d)]} by Th6;
then x = [[(id d),(id d)],(id d)] by TARSKI:def 1;
hence x in the Comp of A by Th5; :: thesis: verum

end;

let a be Object of (1Cat d,(id d)); :: thesis: for b₁ being Element of the carrier of A holds
( not a = b₁ or id a = id b₁ )
let a' be Object of A; :: thesis: ( not a = a' or id a = id a' )
assume a = a' ; :: thesis: id a = id a'
then a' = d by TARSKI:def 1;
hence id a = id a' by TARSKI:def 1; :: thesis: verum