defpred S1[ set , set , set ] means verum;
A2:
for a, b, c being Object of F1() st P1[a] & P1[b] & P1[c] & <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c st S1[a,b,f] & S1[b,c,g] holds
S1[a,c,g * f]
;
A3:
for a being Object of F1() st P1[a] holds
S1[a,a, idm a]
;
A4:
ex a being Object of F1() st P1[a]
by A1;
consider B being non empty strict subcategory of F1() such that
A5:
for a being Object of F1() holds
( a is Object of B iff P1[a] )
and
A6:
for a, b being Object of F1()
for a9, b9 being Object of B st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] )
from YELLOW18:sch 7(A4, A2, A3);
now for a1, a2 being Object of F1()
for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^>let a1,
a2 be
Object of
F1();
for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^>let b1,
b2 be
Object of
B;
( b1 = a1 & b2 = a2 implies <^b1,b2^> = <^a1,a2^> )assume A7:
(
b1 = a1 &
b2 = a2 )
;
<^b1,b2^> = <^a1,a2^>A8:
<^a1,a2^> c= <^b1,b2^>
by A6, A7;
<^b1,b2^> c= <^a1,a2^>
by A7, ALTCAT_2:31;
hence
<^b1,b2^> = <^a1,a2^>
by A8;
verum end;
then
B is full
by Th26;
hence
ex B being non empty strict full subcategory of F1() st
for a being Object of F1() holds
( a is Object of B iff P1[a] )
by A5; verum