consider c being Object of ;
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
for a', b' being Object of st a = a' & b = b' holds
Hom a,b c= Hom a',b' ) & the Comp of (1Cat c,(id c)) c= the Comp of C & ( for a being Object of
for a' being Object of st a = a' holds
id a = id a' ) )

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
for a', b' being Object of st a = a' & b = b' holds
Hom a,b c= Hom a',b' :: thesis: ( the Comp of (1Cat c,(id c)) c= the Comp of C & ( for a being Object of
for a' being Object of st a = a' holds
id a = id a' ) )

proof

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' )
assume ( a = a' & b = b' ) ; :: thesis: Hom a,b c= Hom a',b'
then A1: ( a' = c & b' = 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 a',b' )
assume x in Hom a,b ; :: thesis: x in Hom a',b'
then x = id c by TARSKI:def 1;
hence x in Hom a',b' 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
for a' being Object of st a = a' holds
id a = id a'

proof

reconsider i = id c as Morphism of ;
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 ; :: thesis: for a' being Object of st a = a' holds
id a = id a'
let a' be Object of ; :: thesis: ( a = a' implies id a = id a' )
assume a = a' ; :: thesis: id a = id a'
then a' = c by TARSKI:def 1;
hence id a = id a' 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