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 :: thesis: 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(); :: thesis: for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^>

let b1, b2 be Object of B; :: thesis: ( b1 = a1 & b2 = a2 implies <^b1,b2^> = <^a1,a2^> )
assume A7: ( b1 = a1 & b2 = a2 ) ; :: thesis: <^b1,b2^> = <^a1,a2^>
A8: <^a1,a2^> c= <^b1,b2^> by A6, A7;
<^b1,b2^> c= <^a1,a2^> by ;
hence <^b1,b2^> = <^a1,a2^> by A8; :: thesis: 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; :: thesis: verum