scheme :: ROUGHS_3:sch 1
FinSubIndA1{ F₁() -> non empty finite set , P₁[ Subset of F₁()] } :

for B being Subset of F₁() holds P₁[B]

provided

A1: P₁[ {} F₁()] and
A2: for B9 being Subset of F₁()
for b being Element of F₁() st P₁[B9] & not b in B9 holds
P₁[B9 \/ {b}]