scheme :: YELLOW_3:sch 1
FraenkelA2{ F₁() -> non empty set , F₂( set , set ) -> set , P₁[ set , set ], P₂[ set , set ] } :

{ F₂(s,t) where s, t is Element of F₁() : P₁[s,t] } is Subset of F₁()

provided

A1: for s, t being Element of F₁() holds F₂(s,t) in F₁()