defpred S₁[ set ] means ( $1 is empty or P₁[$1] );
A3: F₂() is finite ;
A4: S₁[ {} ] ;
A5: for x, B being set st x in F₂() & B c= F₂() & S₁[B] holds
S₁[B \/ {x}]

let x, B be set ; :: thesis:
assume that
A6: x in F₂() and
A7: B c= F₂() and
A8: S₁[B] ; :: thesis:
reconsider B = B as Subset of F₁() by A7, XBOOLE_1:1;

suppose x in B ; :: thesis:

then {x} c= B by ZFMISC_1:31;
hence S₁[B \/ {x}] by A8, XBOOLE_1:12; :: thesis:

end;

suppose ( not B is empty & not x in B ) ; :: thesis:

hence S₁[B \/ {x}] by A2, A6, A7, A8; :: thesis:

end;

suppose B is empty ; :: thesis:

hence S₁[B \/ {x}] by A1, A6; :: thesis:

end;

end;

end;

S₁[F₂()] from FINSET_1:sch 2(A3, A4, A5);
hence P₁[F₂()] ; :: thesis: