defpred S_{1}[ set ] means ( $1 is empty 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

hence P