scheme :: FRAENKEL:sch 1
Fraenkel59{ F₁() -> set , F₂( object ) -> object , P₁[ object ], P₂[ object ] } :

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

provided

A1: for v being Element of F₁() st P₁[v] holds
P₂[v]