scheme :: CHAIN_1:sch 4
ChainInd{ F₁() -> non zero Nat, F₂() -> Grating of F₁(), F₃() -> Nat, F₄() -> Chain of F₃(),F₂(), P₁[ set ] } :

A1: P₁[ 0_ (F₃(),F₂())] and
A2: for A being Cell of F₃(),F₂() st A in F₄() holds
P₁[{A}] and
A3: for C1, C2 being Chain of F₃(),F₂() st C1 c= F₄() & C2 c= F₄() & P₁[C1] & P₁[C2] holds
P₁[C1 + C2]