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 a9, b9 being Object of A st a = a9 & b = b9 holds
Hom a,b c= Hom a9,b9 :: 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 a9, b9 being Object of A st a = a9 & b = b9 holds
Hom a,b c= Hom a9,b9
let a9, b9 be Object of A; :: thesis: ( a = a9 & b = b9 implies Hom a,b c= Hom a9,b9 )
assume that
A1: a = a9 and
A2: b = b9 ; :: thesis: Hom a,b c= Hom a9,b9
A3: b9 = d by A2, TARSKI:def 1;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Hom a,b or x in Hom a9,b9 )
assume x in Hom a,b ; :: thesis: x in Hom a9,b9
then A4: x = id d by TARSKI:def 1;
a9 = d by A1, TARSKI:def 1;
hence x in Hom a9,b9 by A3, A4, 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 a9 be Object of A; :: thesis: ( not a = a9 or id a = id a9 )
assume a = a9 ; :: thesis: id a = id a9
then a9 = d by TARSKI:def 1;
hence id a = id a9 by TARSKI:def 1; :: thesis: verum