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

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

provided

A1: for x being Element of F₁() holds P₁[{x}] and
A2: for B1, B2 being non empty Subset of F₁() st P₁[B1] & P₁[B2] holds
P₁[B1 \/ B2]