scheme :: YELLOW_9:sch 1
FraenkelInvolution{ F₁() -> non empty set , F₂() -> Subset of F₁(), F₃() -> Subset of F₁(), F₄( set ) -> Element of F₁() } :

F₂() = { F₄(a) where a is Element of F₁() : a in F₃() }

provided

A1: F₃() = { F₄(a) where a is Element of F₁() : a in F₂() } and
A2: for a being Element of F₁() holds F₄(F₄(a)) = a