defpred S₁[ Nat] means for A being Subset of F₁() st card A = $1 holds
P₁[A];
A2: for n being Nat st ( for i being Nat st i < n holds
S₁[i] ) holds
S₁[n]

proof

let n be Nat; :: thesis: ( ( for i being Nat st i < n holds
S₁[i] ) implies S₁[n] )
assume A3: for i being Nat st i < n holds
S₁[i] ; :: thesis: S₁[n]
let A be Subset of F₁(); :: thesis: ( card A = n implies P₁[A] )
assume A4: card A = n ; :: thesis: P₁[A]

now

let B be set ; :: thesis: ( B c< A implies P₁[B] )
assume A5: B c< A ; :: thesis: P₁[B]
B c= A by A5, XBOOLE_0:def 8;
then reconsider B9 = B as Subset of F₁() by XBOOLE_1:1;
card B9 < n by A4, A5, TREES_1:6;
hence P₁[B] by A3; :: thesis: verum

end;

hence P₁[A] by A1; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 4(A2);
then ( S₁[ card F₁()] & [#] F₁() = F₁() ) ;
hence P₁[F₁()] ; :: thesis: verum