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

proof

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

per cases ( x in B or ( not B is empty & not x in B ) or B is empty ) ;

suppose x in B ; :: thesis: S₁[B \/ {x}]

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

end;

suppose ( not B is empty & not x in B ) ; :: thesis: S₁[B \/ {x}]

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

end;

suppose B is empty ; :: thesis: S₁[B \/ {x}]

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

end;

end;

end;

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