defpred S_{1}[ set ] means ( $1 is trivial or P_{1}[$1] );

A3: F_{2}() is finite
;

A4: S_{1}[ {} ]
;

A5: for x, B being set st x in F_{2}() & B c= F_{2}() & S_{1}[B] holds

S_{1}[B \/ {x}]
_{1}[F_{2}()]
from FINSET_1:sch 2(A3, A4, A5);

hence P_{1}[F_{2}()]
; :: thesis: verum

A3: F

A4: S

A5: for x, B being set st x in F

S

proof

S
let x, B be set ; :: thesis: ( x in F_{2}() & B c= F_{2}() & S_{1}[B] implies S_{1}[B \/ {x}] )

assume that

A6: x in F_{2}()
and

A7: B c= F_{2}()
and

A8: S_{1}[B]
; :: thesis: S_{1}[B \/ {x}]

reconsider B = B as Subset of F_{1}() by A7, XBOOLE_1:1;

end;assume that

A6: x in F

A7: B c= F

A8: S

reconsider B = B as Subset of F

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 ) )
;

end;

suppose A9:
( B is trivial & not B \/ {x} is trivial )
; :: thesis: S_{1}[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_{1}[B \/ {x}]
by A1, A6, A7, A11, A12; :: thesis: verum

end;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

hence P