scheme :: FOMODEL0:sch 4
FraenkelInclusion{ F1() -> set , F2( set , set ) -> set , P1[ set , set ] } :
F1() c= { F2(x,F1()) where x is Element of F1() : P1[x,F1()] }
provided
A1: for y being set st y in F1() holds
ex x being set st
( x in F1() & P1[x,F1()] & y = F2(x,F1()) )