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

P₁[F₁()]

provided

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