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