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 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 ( 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:31;
hence S₁[B \/ {x}] by A8, XBOOLE_1:12; :: thesis: verum

end;

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

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

end;

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

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

end;

end;

end;

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