scheme :: FOMODEL0:sch 4
FraenkelInclusion{ F₁() -> set , F₂( set , set ) -> set , P₁[ set , set ] } :

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

provided

A1: for y being set st y in F₁() holds
ex x being set st
( x in F₁() & P₁[x,F₁()] & y = F₂(x,F₁()) )