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

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}]