defpred S_{1}[ set ] means ex B9 being Subset of F_{1}() st

( B9 = $1 & P_{1}[B9] );

let B be Subset of F_{1}(); :: thesis: P_{1}[B]

A3: for x, A being set st x in B & A c= B & S_{1}[A] holds

S_{1}[A \/ {x}]

A8: S_{1}[ {} ]
by A1;

S_{1}[B]
from FINSET_1:sch 2(A7, A8, A3);

hence P_{1}[B]
; :: thesis: verum

( B9 = $1 & P

let B be Subset of F

A3: for x, A being set st x in B & A c= B & S

S

proof

A7:
B is finite
;
let x, A be set ; :: thesis: ( x in B & A c= B & S_{1}[A] implies S_{1}[A \/ {x}] )

assume that

A4: x in B and

A5: A c= B and

A6: ex B9 being Subset of F_{1}() st

( B9 = A & P_{1}[B9] )
; :: thesis: S_{1}[A \/ {x}]

reconsider x9 = x as Element of F_{1}() by A4;

reconsider A9 = A as Subset of F_{1}() by A5, XBOOLE_1:1;

reconsider A99 = A9 \/ {x9} as Subset of F_{1}() ;

take A99 ; :: thesis: ( A99 = A \/ {x} & P_{1}[A99] )

thus A99 = A \/ {x} ; :: thesis: P_{1}[A99]

thus P_{1}[A99]
by A2, A6, ZFMISC_1:40; :: thesis: verum

end;assume that

A4: x in B and

A5: A c= B and

A6: ex B9 being Subset of F

( B9 = A & P

reconsider x9 = x as Element of F

reconsider A9 = A as Subset of F

reconsider A99 = A9 \/ {x9} as Subset of F

take A99 ; :: thesis: ( A99 = A \/ {x} & P

thus A99 = A \/ {x} ; :: thesis: P

thus P

A8: S

S

hence P