scheme :: NECKLACE:sch 1
Convers{ F₁() -> non empty set , F₂() -> Relation, F₃( set ) -> set , F₄( set ) -> set , P₁[ set ] } :

F₂() ~ = { [F₃(x),F₄(x)] where x is Element of F₁() : P₁[x] }

provided

A1: F₂() = { [F₄(x),F₃(x)] where x is Element of F₁() : P₁[x] }