scheme :: YELLOW20:sch 1
SubcategoryUniq{ F₁() -> category, F₂() -> non empty subcategory of F₁(), F₃() -> non empty subcategory of F₁(), P₁[ set ], P₂[ set , set , set ] } :

AltCatStr(# the carrier of F₂(), the Arrows of F₂(), the Comp of F₂() #) = AltCatStr(# the carrier of F₃(), the Arrows of F₃(), the Comp of F₃() #)

provided

A1: for a being Object of F₁() holds
( a is Object of F₂() iff P₁[a] ) and
A2: for a, b being Object of F₁()
for a9, b9 being Object of F₂() 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] ) and
A3: for a being Object of F₁() holds
( a is Object of F₃() iff P₁[a] ) and
A4: for a, b being Object of F₁()
for a9, b9 being Object of F₃() 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] )