defpred S₁[ set ] means ( $1 <> {} implies ex B' being Element of Fin F₁() st
( B' = $1 & P₁[B'] ) );
let B be non empty Element of Fin 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: ( A <> {} implies ex B' being Element of Fin F₁() st
( B' = A & P₁[B'] ) ) and
A \/ {x} <> {} ; :: thesis: ex B' being Element of Fin F₁() st
( B' = A \/ {x} & P₁[B'] )
reconsider x' = x as Element of F₁() by A4, Th14;
reconsider A' = A as Element of Fin F₁() by A5, Th16;
take A' \/ {.x'.} ; :: thesis: ( A' \/ {.x'.} = A \/ {x} & P₁[A' \/ {.x'.}] )
thus A' \/ {.x'.} = A \/ {x} ; :: thesis: P₁[A' \/ {.x'.}]
A7: P₁[{.x'.}] by A1;

per cases ( A = {} or A <> {} ) ;

suppose A = {} ; :: thesis: P₁[A' \/ {.x'.}]

hence P₁[A' \/ {.x'.}] by A1; :: thesis: verum

end;

suppose A <> {} ; :: thesis: P₁[A' \/ {.x'.}]

hence P₁[A' \/ {.x'.}] by A2, A6, A7; :: thesis: verum

end;

end;

end;

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