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

for i0 being Integer st i0 <= F₁() holds
P₁[i0]

provided

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