defpred S₁[ set ] means ( $1 is trivial 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 A6: ( x in F₂() & B c= F₂() & S₁[B] ) ; :: thesis: S₁[B \/ {x}]
then reconsider B = B as Subset of F₁() by XBOOLE_1:1;

per cases ( B \/ {x} is trivial or x in B or ( not B is trivial & not x in B ) or ( B is trivial & not B \/ {x} is trivial ) ) ;

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

hence S₁[B \/ {x}] ; :: thesis: verum

end;

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

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

end;

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

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

end;

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

then consider y being set such that
A9: B = {y} by Th5;
A10: x <> y by A8, A9;
A11: B \/ {x} = {x,y} by A9, ENUMSET1:41;
y in B by A9, TARSKI:def 1;
hence S₁[B \/ {x}] by A1, A6, A10, A11; :: thesis: verum

end;

end;

end;

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