scheme :: QUANTAL1:sch 2
EmptyFraenkel{ F1() -> non empty set , F2( set ) -> set , P1[ set ] } :
{ F2(a) where a is Element of F1() : P1[a] } = {}
provided
A1: for a being Element of F1() holds P1[a]