ex B being non empty strict subcategory of F₁() st
( ( for a being Object of F₁() holds
( a is Object of B iff P₁[a] ) ) & ( 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 P₂[a,b,f] ) ) )

A1: ex a being Object of F₁() st P₁[a] and
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 P₂[a,b,f] & P₂[b,c,g] holds
P₂[a,c,g * f] and
A3: for a being Object of F₁() st P₁[a] holds
P₂[a,a, idm a]