scheme :: YELLOW20:sch 3
FullSubcategoryUniq{ F₁() -> category, F₂() -> non empty full subcategory of F₁(), F₃() -> non empty full subcategory of F₁(), P₁[ 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 being Object of F₁() holds
( a is Object of F₃() iff P₁[a] )