A3: P₁[ {}. F₁()] by A1;
A4: for B' being Element of Fin F₁()
for b being Element of F₁() st P₁[B'] & not b in B' holds
P₁[B' \/ {b}] by A2;
thus for B being Element of Fin F₁() holds P₁[B] from SETWISEO:sch 2(A3, A4); :: thesis: verum