consider c being Object of C;
set E = 1Cat c,(id c);

now

thus the carrier of (1Cat c,(id c)) c= the carrier of C :: thesis: ( ( for a, b being Object of (1Cat c,(id c))
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom a,b c= Hom a9,b9 ) & the Comp of (1Cat c,(id c)) c= the Comp of C & ( for a being Object of (1Cat c,(id c))
for a9 being Object of C st a = a9 holds
id a = id a9 ) )

proof

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

end;

thus for a, b being Object of (1Cat c,(id c))
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom a,b c= Hom a9,b9 :: thesis: ( the Comp of (1Cat c,(id c)) c= the Comp of C & ( for a being Object of (1Cat c,(id c))
for a9 being Object of C st a = a9 holds
id a = id a9 ) )

proof

let a, b be Object of (1Cat c,(id c)); :: 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 )
assume ( a = a9 & b = b9 ) ; :: thesis: Hom a,b c= Hom a9,b9
then A1: ( a9 = c & b9 = c ) by 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 x = id c by TARSKI:def 1;
hence x in Hom a9,b9 by A1, CAT_1:55; :: thesis: verum

end;

thus the Comp of (1Cat c,(id c)) c= the Comp of C :: thesis: for a being Object of (1Cat c,(id c))
for a9 being Object of C st a = a9 holds
id a = id a9

proof

reconsider i = id c as Morphism of C ;
A2: Hom c,c <> {} by CAT_1:56;
A3: ( dom (id c) = c & cod (id c) = c ) by CAT_1:44;
then A4: [(id c),(id c)] in dom the Comp of C by CAT_1:40;
the Comp of (1Cat c,(id c)) = (id c),(id c) .--> ((id c) * (id c)) by CAT_1:59
.= (id c),(id c) .--> ((id c) * i) by A2, CAT_1:def 13
.= [(id c),(id c)] .--> (the Comp of C . (id c),(id c)) by A3, CAT_1:41 ;
hence the Comp of (1Cat c,(id c)) c= the Comp of C by A4, FUNCT_4:8; :: thesis: verum

end;

let a be Object of (1Cat c,(id c)); :: thesis: for a9 being Object of C st a = a9 holds
id a = id a9
let a9 be Object of C; :: thesis: ( a = a9 implies id a = id a9 )
assume a = a9 ; :: thesis: id a = id a9
then a9 = c by TARSKI:def 1;
hence id a = id a9 by TARSKI:def 1; :: thesis: verum

end;

then 1Cat c,(id c) is Subcategory of C by Def4;
hence ex b₁ being Subcategory of C st b₁ is strict ; :: thesis: verum