scheme :: FOMODEL0:sch 5
FraenkelInclusion2{ F₁() -> set , P₁[ set , set ] } :

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

provided

A1: for x being set st x in F₁() holds
P₁[x,F₁()]