scheme :: INT_1:sch 4
IntIndFull{ F₁() -> Integer, P₁[ Integer] } :

for i0 being Integer holds P₁[i0]

provided

A1: P₁[F₁()] and
A2: for i2 being Integer st P₁[i2] holds
( P₁[i2 - 1] & P₁[i2 + 1] )