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

now

let a1, a2 be object of ; :: thesis: for b1, b2 being object of st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^>
let b1, b2 be object of ; :: 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^>

proof

let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in <^a1,a2^> or f in <^b1,b2^> )
assume f in <^a1,a2^> ; :: thesis: f in <^b1,b2^>
hence f in <^b1,b2^> by A6, A7; :: thesis: verum

end;

<^b1,b2^> c= <^a1,a2^> by A7, ALTCAT_2:32;
hence <^b1,b2^> = <^a1,a2^> by A8, XBOOLE_0:def 10; :: thesis: verum

end;

then B is full by Th27;
hence ex B being non empty strict full subcategory of non empty strict full st
for a being object of holds
( a is object of iff P₁[a] ) by A5; :: thesis: verum