defpred S₁[ Nat] means for H being ZF-formula st len H = $1 holds
P₁[H];
A2: for n being Nat st ( for k being Nat st k < n holds
S₁[k] ) holds
S₁[n]

proof

let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S₁[k] ) implies S₁[n] )
assume A3: for k being Nat st k < n holds
for H being ZF-formula st len H = k holds
P₁[H] ; :: thesis: S₁[n]
let H be ZF-formula; :: thesis: ( len H = n implies P₁[H] )
assume A4: len H = n ; :: thesis: P₁[H]

now :: thesis: for F being ZF-formula st F is_proper_subformula_of H holds
P₁[F]

let F be ZF-formula; :: thesis: ( F is_proper_subformula_of H implies P₁[F] )
assume F is_proper_subformula_of H ; :: thesis: P₁[F]
then len F < len H by Th62;
hence P₁[F] by A3, A4; :: thesis: verum

end;

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

end;

A5: for n being Nat holds S₁[n] from NAT_1:sch 4(A2);
let H be ZF-formula; :: thesis: P₁[H]
len H = len H ;
hence P₁[H] by A5; :: thesis: verum