scheme :: STACKS_1:sch 6
PathIND{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> Relation of F₁(), P₁[ set ] } :

A1: P₁[F₂()] and
A2: F₄() reduces F₂(),F₃() and
A3: for x, y being Element of F₁() st F₄() reduces F₂(),x & [x,y] in F₄() & P₁[x] holds
P₁[y]