A3: 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;
A4: P₁[ {}. F₁()] by A1;
thus for B being Element of Fin F₁() holds P₁[B] from SETWISEO:sch 2(A4, A3); :: thesis: verum