A3: for B9 being Element of Fin F₁()
for b being Element of F₁() st P₁[B9] & not b in B9 holds
P₁[B9 \/ {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