defpred S₁[ set ] means ex B9 being Subset of F₁() st
( B9 = $1 & P₁[B9] );
let B be Subset of F₁(); :: thesis: P₁[B]
A3: for x, A being set st x in B & A c= B & S₁[A] holds
S₁[A \/ {x}]

proof

let x, A be set ; :: thesis: ( x in B & A c= B & S₁[A] implies S₁[A \/ {x}] )
assume that
A4: x in B and
A5: A c= B and
A6: ex B9 being Subset of F₁() st
( B9 = A & P₁[B9] ) ; :: thesis: S₁[A \/ {x}]
reconsider x9 = x as Element of F₁() by A4;
reconsider A9 = A as Subset of F₁() by A5, XBOOLE_1:1;
reconsider A99 = A9 \/ {x9} as Subset of F₁() ;
take A99 ; :: thesis: ( A99 = A \/ {x} & P₁[A99] )
thus A99 = A \/ {x} ; :: thesis: P₁[A99]
thus P₁[A99] by A2, A6, ZFMISC_1:40; :: thesis: verum

end;

A7: B is finite ;
A8: S₁[ {} ] by A1;
S₁[B] from FINSET_1:sch 2(A7, A8, A3);
hence P₁[B] ; :: thesis: verum