defpred S1[ Nat] means for A being Subset of F1() st card A = $1 holds
P1[A];
A2:
for n being Nat st ( for i being Nat st i < n holds
S1[i] ) holds
S1[n]
proof
let n be
Nat;
( ( for i being Nat st i < n holds
S1[i] ) implies S1[n] )
assume A3:
for
i being
Nat st
i < n holds
S1[
i]
;
S1[n]
let A be
Subset of
F1();
( card A = n implies P1[A] )
assume A4:
card A = n
;
P1[A]
now for B being set st B c< A holds
P1[B]end;
hence
P1[
A]
by A1;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 4(A2);
then
( S1[ card F1()] & [#] F1() = F1() )
;
hence
P1[F1()]
; verum