scheme :: MSAFREE4:sch 5
A{ F₁() -> set , F₂() -> set , F₃() -> Relation, P₁[ set ] } :

A1: P₁[F₁()] and
A2: F₃() reduces F₁(),F₂() and
A3: for y, z being set st F₃() reduces F₁(),y & [y,z] in F₃() & P₁[y] holds
P₁[z]