scheme :: CHAIN_1:sch 1
FrSet12{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ], F₃( set , set ) -> Element of F₁() } :

{ F₃(x,y) where x, y is Element of F₂() : P₁[x,y] } c= F₁()