defpred S₁[ set , set , set ] means verum;
A2: for a, b, c being Object of F₁() st P₁[a] & P₁[b] & P₁[c] & <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c st S₁[a,b,f] & S₁[b,c,g] holds
S₁[a,c,g * f] ;
A3: for a being Object of F₁() st P₁[a] holds
S₁[a,a, idm a] ;
A4: ex a being Object of F₁() st P₁[a] by A1;
consider B being non empty strict subcategory of F₁() such that
A5: for a being Object of F₁() holds
( a is Object of B iff P₁[a] ) and
A6: for a, b being Object of F₁()
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 S₁[a,b,f] ) from YELLOW18:sch 7(A4, A2, A3);

now :: thesis: for a1, a2 being Object of F₁()
for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^>

let a1, a2 be Object of F₁(); :: 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 A7, ALTCAT_2:31;
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 F₁() st
for a being Object of F₁() holds
( a is Object of B iff P₁[a] ) by A5; :: thesis: verum