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; :: thesis: ( ( 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] ; :: thesis: S1[n]
let A be Subset of F1(); :: thesis: ( card A = n implies P1[A] )
assume A4: card A = n ; :: thesis: P1[A]
now :: thesis: for B being set st B c< A holds
P1[B]
let B be set ; :: thesis: ( B c< A implies P1[B] )
assume A5: B c< A ; :: thesis: P1[B]
B c= A by A5;
then reconsider B9 = B as Subset of F1() by XBOOLE_1:1;
card B9 < n by A4, A5, TREES_1:6;
hence P1[B] by A3; :: thesis: verum
end;
hence P1[A] by A1; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 4(A2);
 then ( S1[ card F1()] & [#] F1() = F1() ) ;
hence P1[F1()] ; :: thesis: verum