scheme :: FRAENKEL:sch 1
Fraenkel59{ F1() -> set , F2( object ) -> object , P1[ object ], P2[ object ] } :
{ F2(v) where v is Element of F1() : P1[v] } c= { F2(u) where u is Element of F1() : P2[u] }
provided
A1: for v being Element of F1() st P1[v] holds
P2[v]